Theorem ralunb 4129

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1539   ∈ wcel 2109  ∀wral 3065   ∪ cun 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3432  df-un 3896

This theorem is referenced by:  ralun  4130  raldifeq  4429  ralprgf  4633  ralprg  4635  raltpg  4639  ralunsn  4830  disjxun  5076  undifixp  8696  ixpfi2  9078  dffi3  9151  fseqenlem1  9764  hashf1lem1  14149  hashf1lem1OLD  14150  pfxsuffeqwrdeq  14392  rexfiuz  15040  modfsummods  15486  modfsummod  15487  coprmproddvdslem  16348  prmind2  16371  prmreclem2  16599  lubun  18214  efgsp1  19324  unocv  20866  coe1fzgsumdlem  21453  evl1gsumdlem  21503  basdif0  22084  isclo  22219  ordtrest2  22336  ptbasfi  22713  ptcnplem  22753  ptrescn  22771  ordthmeolem  22933  prdsxmetlem  23502  prdsbl  23628  iblcnlem1  24933  ellimc2  25022  rlimcnp  26096  xrlimcnp  26099  ftalem3  26205  dchreq  26387  2sqlem10  26557  dchrisum0flb  26639  pntpbnd1  26715  wlkp1lem8  28028  pthdlem1  28113  crctcshwlkn0lem7  28160  wwlksnext  28237  clwwlkccatlem  28332  clwwlkel  28389  clwwlkwwlksb  28397  wwlksext2clwwlk  28400  clwwlknonex2lem2  28451  3wlkdlem4  28505  3pthdlem1  28507  upgr4cycl4dv4e  28528  dfconngr1  28531  cntzun  31299  ordtrest2NEW  31852  subfacp1lem3  33123  subfacp1lem5  33125  erdszelem8  33139  hfext  34464  bj-raldifsn  35250  finixpnum  35741  lindsadd  35749  lindsenlbs  35751  poimirlem26  35782  poimirlem27  35783  poimirlem32  35788  prdsbnd  35930  rrnequiv  35972  hdmap14lem13  39873