Theorem ralunb 4158

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 4145	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1846	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1897	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3086	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3086	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3086	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 639	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 306	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   ∈ wcel 2149  ∀wral 3085   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-v 3465  df-un 3918

This theorem is referenced by:  ralun  4159  raldifeq  4456  ralprgf  4662  ralprg  4664  raltpg  4666  ralunsn  4860  disjxun  5108  naddunif  8676  undifixp  8928  ixpfi2  9303  dffi3  9387  fseqenlem1  10004  hashf1lem1  14488  pfxsuffeqwrdeq  14731  rexfiuz  15395  modfsummods  15841  modfsummod  15842  coprmproddvdslem  16716  prmind2  16739  prmreclem2  16973  lubun  18567  efgsp1  19803  unocv  21795  coe1fzgsumdlem  22428  evl1gsumdlem  22481  basdif0  23075  isclo  23209  ordtrest2  23326  ptbasfi  23703  ptcnplem  23743  ptrescn  23761  ordthmeolem  23923  prdsxmetlem  24490  prdsbl  24613  iblcnlem1  25912  ellimc2  26001  rlimcnp  27092  xrlimcnp  27095  ftalem3  27201  dchreq  27384  2sqlem10  27554  dchrisum0flb  27636  pntpbnd1  27712  addsuniflem  28156  mulsuniflem  28304  pw2cut2  28617  elreno2  28650  wlkp1lem8  29965  pthdlem1  30052  crctcshwlkn0lem7  30102  wwlksnext  30179  clwwlkccatlem  30277  clwwlkel  30334  clwwlkwwlksb  30342  wwlksext2clwwlk  30345  clwwlknonex2lem2  30396  3wlkdlem4  30450  3pthdlem1  30452  upgr4cycl4dv4e  30473  dfconngr1  30476  cntzun  33336  ordtrest2NEW  34254  subfacp1lem3  35569  subfacp1lem5  35571  erdszelem8  35585  hfext  36570  bj-raldifsn  37625  finixpnum  38139  lindsadd  38147  lindsenlbs  38149  poimirlem26  38180  poimirlem27  38181  poimirlem32  38186  prdsbnd  38327  rrnequiv  38369  hdmap14lem13  42539  usgrexmpl1lem  48668  usgrexmpl2lem  48673  usgrexmpl2trifr  48684