Theorem ralunb 4191

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 4178	. . . 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 3946

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 3953

This theorem is referenced by:  ralun  4192  raldifeq  4493  ralprgf  4696  ralprg  4698  raltpg  4702  ralunsn  4894  disjxun  5146  naddunif  8689  undifixp  8925  ixpfi2  9347  dffi3  9423  fseqenlem1  10016  hashf1lem1  14412  hashf1lem1OLD  14413  pfxsuffeqwrdeq  14645  rexfiuz  15291  modfsummods  15736  modfsummod  15737  coprmproddvdslem  16596  prmind2  16619  prmreclem2  16847  lubun  18465  efgsp1  19600  unocv  21225  coe1fzgsumdlem  21817  evl1gsumdlem  21867  basdif0  22448  isclo  22583  ordtrest2  22700  ptbasfi  23077  ptcnplem  23117  ptrescn  23135  ordthmeolem  23297  prdsxmetlem  23866  prdsbl  23992  iblcnlem1  25297  ellimc2  25386  rlimcnp  26460  xrlimcnp  26463  ftalem3  26569  dchreq  26751  2sqlem10  26921  dchrisum0flb  27003  pntpbnd1  27079  addsuniflem  27474  mulsuniflem  27594  wlkp1lem8  28927  pthdlem1  29013  crctcshwlkn0lem7  29060  wwlksnext  29137  clwwlkccatlem  29232  clwwlkel  29289  clwwlkwwlksb  29297  wwlksext2clwwlk  29300  clwwlknonex2lem2  29351  3wlkdlem4  29405  3pthdlem1  29407  upgr4cycl4dv4e  29428  dfconngr1  29431  cntzun  32200  ordtrest2NEW  32892  subfacp1lem3  34162  subfacp1lem5  34164  erdszelem8  34178  hfext  35144  bj-raldifsn  35970  finixpnum  36462  lindsadd  36470  lindsenlbs  36472  poimirlem26  36503  poimirlem27  36504  poimirlem32  36509  prdsbnd  36650  rrnequiv  36692  hdmap14lem13  40740