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  4459  ralprgf  4665  ralprg  4667  raltpg  4669  ralunsn  4863  disjxun  5111  naddunif  8682  undifixp  8934  ixpfi2  9309  dffi3  9393  fseqenlem1  10010  hashf1lem1  14494  pfxsuffeqwrdeq  14737  rexfiuz  15401  modfsummods  15847  modfsummod  15848  coprmproddvdslem  16722  prmind2  16745  prmreclem2  16979  lubun  18573  efgsp1  19809  unocv  21801  coe1fzgsumdlem  22434  evl1gsumdlem  22487  basdif0  23081  isclo  23215  ordtrest2  23332  ptbasfi  23709  ptcnplem  23749  ptrescn  23767  ordthmeolem  23929  prdsxmetlem  24496  prdsbl  24619  iblcnlem1  25918  ellimc2  26007  rlimcnp  27098  xrlimcnp  27101  ftalem3  27207  dchreq  27390  2sqlem10  27560  dchrisum0flb  27642  pntpbnd1  27718  addsuniflem  28162  mulsuniflem  28310  pw2cut2  28623  elreno2  28656  wlkp1lem8  29971  pthdlem1  30058  crctcshwlkn0lem7  30108  wwlksnext  30185  clwwlkccatlem  30283  clwwlkel  30340  clwwlkwwlksb  30348  wwlksext2clwwlk  30351  clwwlknonex2lem2  30402  3wlkdlem4  30456  3pthdlem1  30458  upgr4cycl4dv4e  30479  dfconngr1  30482  cntzun  33342  ordtrest2NEW  34260  subfacp1lem3  35609  subfacp1lem5  35611  erdszelem8  35625  hfext  36610  bj-raldifsn  37667  finixpnum  38181  lindsadd  38189  lindsenlbs  38191  poimirlem26  38222  poimirlem27  38223  poimirlem32  38228  prdsbnd  38369  rrnequiv  38411  hdmap14lem13  42581  usgrexmpl1lem  48712  usgrexmpl2lem  48717  usgrexmpl2trifr  48728