Theorem ralunb 4156

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 4143	. . . 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 3909

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 3446  df-un 3916

This theorem is referenced by:  ralun  4157  raldifeq  4453  ralprgf  4654  ralprg  4656  raltpg  4658  ralunsn  4854  disjxun  5100  naddunif  8634  undifixp  8884  ixpfi2  9277  dffi3  9358  fseqenlem1  9953  hashf1lem1  14396  pfxsuffeqwrdeq  14639  rexfiuz  15290  modfsummods  15735  modfsummod  15736  coprmproddvdslem  16608  prmind2  16631  prmreclem2  16864  lubun  18456  efgsp1  19651  unocv  21622  coe1fzgsumdlem  22223  evl1gsumdlem  22276  basdif0  22873  isclo  23007  ordtrest2  23124  ptbasfi  23501  ptcnplem  23541  ptrescn  23559  ordthmeolem  23721  prdsxmetlem  24289  prdsbl  24412  iblcnlem1  25722  ellimc2  25811  rlimcnp  26908  xrlimcnp  26911  ftalem3  27018  dchreq  27202  2sqlem10  27372  dchrisum0flb  27454  pntpbnd1  27530  addsuniflem  27948  mulsuniflem  28092  wlkp1lem8  29659  pthdlem1  29746  crctcshwlkn0lem7  29796  wwlksnext  29873  clwwlkccatlem  29968  clwwlkel  30025  clwwlkwwlksb  30033  wwlksext2clwwlk  30036  clwwlknonex2lem2  30087  3wlkdlem4  30141  3pthdlem1  30143  upgr4cycl4dv4e  30164  dfconngr1  30167  cntzun  33051  ordtrest2NEW  33906  subfacp1lem3  35162  subfacp1lem5  35164  erdszelem8  35178  hfext  36164  bj-raldifsn  37081  finixpnum  37592  lindsadd  37600  lindsenlbs  37602  poimirlem26  37633  poimirlem27  37634  poimirlem32  37639  prdsbnd  37780  rrnequiv  37822  hdmap14lem13  41867  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2trifr  48021