Theorem ralunb 4160

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 4147	. . . 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 3912

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 3449  df-un 3919

This theorem is referenced by:  ralun  4161  raldifeq  4457  ralprgf  4658  ralprg  4660  raltpg  4662  ralunsn  4858  disjxun  5105  naddunif  8657  undifixp  8907  ixpfi2  9301  dffi3  9382  fseqenlem1  9977  hashf1lem1  14420  pfxsuffeqwrdeq  14663  rexfiuz  15314  modfsummods  15759  modfsummod  15760  coprmproddvdslem  16632  prmind2  16655  prmreclem2  16888  lubun  18474  efgsp1  19667  unocv  21589  coe1fzgsumdlem  22190  evl1gsumdlem  22243  basdif0  22840  isclo  22974  ordtrest2  23091  ptbasfi  23468  ptcnplem  23508  ptrescn  23526  ordthmeolem  23688  prdsxmetlem  24256  prdsbl  24379  iblcnlem1  25689  ellimc2  25778  rlimcnp  26875  xrlimcnp  26878  ftalem3  26985  dchreq  27169  2sqlem10  27339  dchrisum0flb  27421  pntpbnd1  27497  addsuniflem  27908  mulsuniflem  28052  wlkp1lem8  29608  pthdlem1  29696  crctcshwlkn0lem7  29746  wwlksnext  29823  clwwlkccatlem  29918  clwwlkel  29975  clwwlkwwlksb  29983  wwlksext2clwwlk  29986  clwwlknonex2lem2  30037  3wlkdlem4  30091  3pthdlem1  30093  upgr4cycl4dv4e  30114  dfconngr1  30117  cntzun  33008  ordtrest2NEW  33913  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem8  35185  hfext  36171  bj-raldifsn  37088  finixpnum  37599  lindsadd  37607  lindsenlbs  37609  poimirlem26  37640  poimirlem27  37641  poimirlem32  37646  prdsbnd  37787  rrnequiv  37829  hdmap14lem13  41874  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2trifr  48028