Theorem ralunb 4144

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2111  ∀wral 3047   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-un 3902

This theorem is referenced by:  ralun  4145  raldifeq  4441  ralprgf  4644  ralprg  4646  raltpg  4648  ralunsn  4843  disjxun  5087  naddunif  8608  undifixp  8858  ixpfi2  9234  dffi3  9315  fseqenlem1  9915  hashf1lem1  14362  pfxsuffeqwrdeq  14605  rexfiuz  15255  modfsummods  15700  modfsummod  15701  coprmproddvdslem  16573  prmind2  16596  prmreclem2  16829  lubun  18421  efgsp1  19649  unocv  21617  coe1fzgsumdlem  22218  evl1gsumdlem  22271  basdif0  22868  isclo  23002  ordtrest2  23119  ptbasfi  23496  ptcnplem  23536  ptrescn  23554  ordthmeolem  23716  prdsxmetlem  24283  prdsbl  24406  iblcnlem1  25716  ellimc2  25805  rlimcnp  26902  xrlimcnp  26905  ftalem3  27012  dchreq  27196  2sqlem10  27366  dchrisum0flb  27448  pntpbnd1  27524  addsuniflem  27944  mulsuniflem  28088  pw2cut2  28382  wlkp1lem8  29657  pthdlem1  29744  crctcshwlkn0lem7  29794  wwlksnext  29871  clwwlkccatlem  29969  clwwlkel  30026  clwwlkwwlksb  30034  wwlksext2clwwlk  30037  clwwlknonex2lem2  30088  3wlkdlem4  30142  3pthdlem1  30144  upgr4cycl4dv4e  30165  dfconngr1  30168  cntzun  33048  ordtrest2NEW  33936  subfacp1lem3  35226  subfacp1lem5  35228  erdszelem8  35242  hfext  36227  bj-raldifsn  37144  finixpnum  37644  lindsadd  37652  lindsenlbs  37654  poimirlem26  37685  poimirlem27  37686  poimirlem32  37691  prdsbnd  37832  rrnequiv  37874  hdmap14lem13  41978  usgrexmpl1lem  48120  usgrexmpl2lem  48125  usgrexmpl2trifr  48136