Theorem ralunb 4187

Description: Restricted quantification over a union. (Contributed by Scott Fenton, 12-Apr-2011.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
ralunb	⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Proof of Theorem ralunb

Step	Hyp	Ref	Expression
1		elunant 4174	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1814	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1866	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3057	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3057	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3057	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 626	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 303	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1532   ∈ wcel 2099  ∀wral 3056   ∪ cun 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-v 3471  df-un 3949

This theorem is referenced by:  ralun  4188  raldifeq  4489  ralprgf  4692  ralprg  4694  raltpg  4698  ralunsn  4890  disjxun  5140  naddunif  8707  undifixp  8944  ixpfi2  9366  dffi3  9446  fseqenlem1  10039  hashf1lem1  14439  hashf1lem1OLD  14440  pfxsuffeqwrdeq  14672  rexfiuz  15318  modfsummods  15763  modfsummod  15764  coprmproddvdslem  16624  prmind2  16647  prmreclem2  16877  lubun  18498  efgsp1  19683  unocv  21599  coe1fzgsumdlem  22209  evl1gsumdlem  22262  basdif0  22843  isclo  22978  ordtrest2  23095  ptbasfi  23472  ptcnplem  23512  ptrescn  23530  ordthmeolem  23692  prdsxmetlem  24261  prdsbl  24387  iblcnlem1  25704  ellimc2  25793  rlimcnp  26884  xrlimcnp  26887  ftalem3  26994  dchreq  27178  2sqlem10  27348  dchrisum0flb  27430  pntpbnd1  27506  addsuniflem  27905  mulsuniflem  28036  wlkp1lem8  29481  pthdlem1  29567  crctcshwlkn0lem7  29614  wwlksnext  29691  clwwlkccatlem  29786  clwwlkel  29843  clwwlkwwlksb  29851  wwlksext2clwwlk  29854  clwwlknonex2lem2  29905  3wlkdlem4  29959  3pthdlem1  29961  upgr4cycl4dv4e  29982  dfconngr1  29985  cntzun  32752  ordtrest2NEW  33460  subfacp1lem3  34728  subfacp1lem5  34730  erdszelem8  34744  hfext  35715  bj-raldifsn  36515  finixpnum  37013  lindsadd  37021  lindsenlbs  37023  poimirlem26  37054  poimirlem27  37055  poimirlem32  37060  prdsbnd  37201  rrnequiv  37243  hdmap14lem13  41290