Theorem ralunb 4192

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 4179	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1822	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1874	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3063	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3063	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 628	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 303	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   ∈ wcel 2107  ∀wral 3062   ∪ cun 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-un 3954

This theorem is referenced by:  ralun  4193  raldifeq  4494  ralprgf  4697  ralprg  4699  raltpg  4703  ralunsn  4895  disjxun  5147  naddunif  8692  undifixp  8928  ixpfi2  9350  dffi3  9426  fseqenlem1  10019  hashf1lem1  14415  hashf1lem1OLD  14416  pfxsuffeqwrdeq  14648  rexfiuz  15294  modfsummods  15739  modfsummod  15740  coprmproddvdslem  16599  prmind2  16622  prmreclem2  16850  lubun  18468  efgsp1  19605  unocv  21233  coe1fzgsumdlem  21825  evl1gsumdlem  21875  basdif0  22456  isclo  22591  ordtrest2  22708  ptbasfi  23085  ptcnplem  23125  ptrescn  23143  ordthmeolem  23305  prdsxmetlem  23874  prdsbl  24000  iblcnlem1  25305  ellimc2  25394  rlimcnp  26470  xrlimcnp  26473  ftalem3  26579  dchreq  26761  2sqlem10  26931  dchrisum0flb  27013  pntpbnd1  27089  addsuniflem  27484  mulsuniflem  27604  wlkp1lem8  28937  pthdlem1  29023  crctcshwlkn0lem7  29070  wwlksnext  29147  clwwlkccatlem  29242  clwwlkel  29299  clwwlkwwlksb  29307  wwlksext2clwwlk  29310  clwwlknonex2lem2  29361  3wlkdlem4  29415  3pthdlem1  29417  upgr4cycl4dv4e  29438  dfconngr1  29441  cntzun  32212  ordtrest2NEW  32903  subfacp1lem3  34173  subfacp1lem5  34175  erdszelem8  34189  hfext  35155  bj-raldifsn  35981  finixpnum  36473  lindsadd  36481  lindsenlbs  36483  poimirlem26  36514  poimirlem27  36515  poimirlem32  36520  prdsbnd  36661  rrnequiv  36703  hdmap14lem13  40751