Theorem ralunb 4148

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 4135	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1870	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3045	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3045	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3045	. . 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 3044   ∪ cun 3901

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3438  df-un 3908

This theorem is referenced by:  ralun  4149  raldifeq  4445  ralprgf  4646  ralprg  4648  raltpg  4650  ralunsn  4845  disjxun  5090  naddunif  8611  undifixp  8861  ixpfi2  9240  dffi3  9321  fseqenlem1  9918  hashf1lem1  14362  pfxsuffeqwrdeq  14604  rexfiuz  15255  modfsummods  15700  modfsummod  15701  coprmproddvdslem  16573  prmind2  16596  prmreclem2  16829  lubun  18421  efgsp1  19616  unocv  21587  coe1fzgsumdlem  22188  evl1gsumdlem  22241  basdif0  22838  isclo  22972  ordtrest2  23089  ptbasfi  23466  ptcnplem  23506  ptrescn  23524  ordthmeolem  23686  prdsxmetlem  24254  prdsbl  24377  iblcnlem1  25687  ellimc2  25776  rlimcnp  26873  xrlimcnp  26876  ftalem3  26983  dchreq  27167  2sqlem10  27337  dchrisum0flb  27419  pntpbnd1  27495  addsuniflem  27913  mulsuniflem  28057  wlkp1lem8  29624  pthdlem1  29711  crctcshwlkn0lem7  29761  wwlksnext  29838  clwwlkccatlem  29933  clwwlkel  29990  clwwlkwwlksb  29998  wwlksext2clwwlk  30001  clwwlknonex2lem2  30052  3wlkdlem4  30106  3pthdlem1  30108  upgr4cycl4dv4e  30129  dfconngr1  30132  cntzun  33022  ordtrest2NEW  33896  subfacp1lem3  35165  subfacp1lem5  35167  erdszelem8  35181  hfext  36167  bj-raldifsn  37084  finixpnum  37595  lindsadd  37603  lindsenlbs  37605  poimirlem26  37636  poimirlem27  37637  poimirlem32  37642  prdsbnd  37783  rrnequiv  37825  hdmap14lem13  41869  usgrexmpl1lem  48015  usgrexmpl2lem  48020  usgrexmpl2trifr  48031