Theorem ralunb 4189

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 4176	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1813	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1865	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 274	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3051	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3051	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3051	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 626	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 302	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1531   ∈ wcel 2098  ∀wral 3050   ∪ cun 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-un 3949

This theorem is referenced by:  ralun  4190  raldifeq  4495  ralprgf  4698  ralprg  4700  raltpg  4704  ralunsn  4896  disjxun  5147  naddunif  8714  undifixp  8953  ixpfi2  9381  dffi3  9461  fseqenlem1  10054  hashf1lem1  14456  hashf1lem1OLD  14457  pfxsuffeqwrdeq  14689  rexfiuz  15335  modfsummods  15780  modfsummod  15781  coprmproddvdslem  16641  prmind2  16664  prmreclem2  16894  lubun  18515  efgsp1  19709  unocv  21634  coe1fzgsumdlem  22252  evl1gsumdlem  22305  basdif0  22905  isclo  23040  ordtrest2  23157  ptbasfi  23534  ptcnplem  23574  ptrescn  23592  ordthmeolem  23754  prdsxmetlem  24323  prdsbl  24449  iblcnlem1  25766  ellimc2  25855  rlimcnp  26947  xrlimcnp  26950  ftalem3  27057  dchreq  27241  2sqlem10  27411  dchrisum0flb  27493  pntpbnd1  27569  addsuniflem  27969  mulsuniflem  28104  wlkp1lem8  29571  pthdlem1  29657  crctcshwlkn0lem7  29704  wwlksnext  29781  clwwlkccatlem  29876  clwwlkel  29933  clwwlkwwlksb  29941  wwlksext2clwwlk  29944  clwwlknonex2lem2  29995  3wlkdlem4  30049  3pthdlem1  30051  upgr4cycl4dv4e  30072  dfconngr1  30075  cntzun  32869  ordtrest2NEW  33657  subfacp1lem3  34925  subfacp1lem5  34927  erdszelem8  34941  hfext  35912  bj-raldifsn  36712  finixpnum  37211  lindsadd  37219  lindsenlbs  37221  poimirlem26  37252  poimirlem27  37253  poimirlem32  37258  prdsbnd  37399  rrnequiv  37441  hdmap14lem13  41485