Theorem ralunb 4163

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  ∀wral 3045   ∪ cun 3915

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-un 3922

This theorem is referenced by:  ralun  4164  raldifeq  4460  ralprgf  4661  ralprg  4663  raltpg  4665  ralunsn  4861  disjxun  5108  naddunif  8660  undifixp  8910  ixpfi2  9308  dffi3  9389  fseqenlem1  9984  hashf1lem1  14427  pfxsuffeqwrdeq  14670  rexfiuz  15321  modfsummods  15766  modfsummod  15767  coprmproddvdslem  16639  prmind2  16662  prmreclem2  16895  lubun  18481  efgsp1  19674  unocv  21596  coe1fzgsumdlem  22197  evl1gsumdlem  22250  basdif0  22847  isclo  22981  ordtrest2  23098  ptbasfi  23475  ptcnplem  23515  ptrescn  23533  ordthmeolem  23695  prdsxmetlem  24263  prdsbl  24386  iblcnlem1  25696  ellimc2  25785  rlimcnp  26882  xrlimcnp  26885  ftalem3  26992  dchreq  27176  2sqlem10  27346  dchrisum0flb  27428  pntpbnd1  27504  addsuniflem  27915  mulsuniflem  28059  wlkp1lem8  29615  pthdlem1  29703  crctcshwlkn0lem7  29753  wwlksnext  29830  clwwlkccatlem  29925  clwwlkel  29982  clwwlkwwlksb  29990  wwlksext2clwwlk  29993  clwwlknonex2lem2  30044  3wlkdlem4  30098  3pthdlem1  30100  upgr4cycl4dv4e  30121  dfconngr1  30124  cntzun  33015  ordtrest2NEW  33920  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem8  35192  hfext  36178  bj-raldifsn  37095  finixpnum  37606  lindsadd  37614  lindsenlbs  37616  poimirlem26  37647  poimirlem27  37648  poimirlem32  37653  prdsbnd  37794  rrnequiv  37836  hdmap14lem13  41881  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2trifr  48032