Theorem ralunb 4170

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 4157	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1870	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 277	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3146	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3146	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3146	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 628	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 305	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1534   ∈ wcel 2113  ∀wral 3141   ∪ cun 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-v 3499  df-un 3944

This theorem is referenced by:  ralun  4171  raldifeq  4442  ralprgf  4633  raltpg  4637  ralunsn  4827  disjxun  5067  undifixp  8501  ixpfi2  8825  dffi3  8898  fseqenlem1  9453  hashf1lem1  13816  pfxsuffeqwrdeq  14063  rexfiuz  14710  modfsummods  15151  modfsummod  15152  coprmproddvdslem  16009  prmind2  16032  prmreclem2  16256  lubun  17736  efgsp1  18866  coe1fzgsumdlem  20472  evl1gsumdlem  20522  unocv  20827  basdif0  21564  isclo  21698  ordtrest2  21815  ptbasfi  22192  ptcnplem  22232  ptrescn  22250  ordthmeolem  22412  prdsxmetlem  22981  prdsbl  23104  iblcnlem1  24391  ellimc2  24478  rlimcnp  25546  xrlimcnp  25549  ftalem3  25655  dchreq  25837  2sqlem10  26007  dchrisum0flb  26089  pntpbnd1  26165  wlkp1lem8  27465  pthdlem1  27550  crctcshwlkn0lem7  27597  wwlksnext  27674  clwwlkccatlem  27770  clwwlkel  27828  clwwlkwwlksb  27836  wwlksext2clwwlk  27839  clwwlknonex2lem2  27890  3wlkdlem4  27944  3pthdlem1  27946  upgr4cycl4dv4e  27967  dfconngr1  27970  cntzun  30699  ordtrest2NEW  31170  subfacp1lem3  32433  subfacp1lem5  32435  erdszelem8  32449  ssltun1  33273  ssltun2  33274  hfext  33648  bj-raldifsn  34396  finixpnum  34881  lindsadd  34889  lindsenlbs  34891  poimirlem26  34922  poimirlem27  34923  poimirlem32  34928  prdsbnd  35075  rrnequiv  35117  hdmap14lem13  39020