Theorem ralunb 4197

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 4184	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1870	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3062	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3062	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3062	. . 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 2108  ∀wral 3061   ∪ cun 3949

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-un 3956

This theorem is referenced by:  ralun  4198  raldifeq  4494  ralprgf  4694  ralprg  4696  raltpg  4698  ralunsn  4894  disjxun  5141  naddunif  8731  undifixp  8974  ixpfi2  9390  dffi3  9471  fseqenlem1  10064  hashf1lem1  14494  pfxsuffeqwrdeq  14736  rexfiuz  15386  modfsummods  15829  modfsummod  15830  coprmproddvdslem  16699  prmind2  16722  prmreclem2  16955  lubun  18560  efgsp1  19755  unocv  21698  coe1fzgsumdlem  22307  evl1gsumdlem  22360  basdif0  22960  isclo  23095  ordtrest2  23212  ptbasfi  23589  ptcnplem  23629  ptrescn  23647  ordthmeolem  23809  prdsxmetlem  24378  prdsbl  24504  iblcnlem1  25823  ellimc2  25912  rlimcnp  27008  xrlimcnp  27011  ftalem3  27118  dchreq  27302  2sqlem10  27472  dchrisum0flb  27554  pntpbnd1  27630  addsuniflem  28034  mulsuniflem  28175  wlkp1lem8  29698  pthdlem1  29786  crctcshwlkn0lem7  29836  wwlksnext  29913  clwwlkccatlem  30008  clwwlkel  30065  clwwlkwwlksb  30073  wwlksext2clwwlk  30076  clwwlknonex2lem2  30127  3wlkdlem4  30181  3pthdlem1  30183  upgr4cycl4dv4e  30204  dfconngr1  30207  cntzun  33071  ordtrest2NEW  33922  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem8  35203  hfext  36184  bj-raldifsn  37101  finixpnum  37612  lindsadd  37620  lindsenlbs  37622  poimirlem26  37653  poimirlem27  37654  poimirlem32  37659  prdsbnd  37800  rrnequiv  37842  hdmap14lem13  41882  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2trifr  47996