Theorem ralunb 4151

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 4138	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1872	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 275	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3053	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 629	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 303	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3052   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-un 3908

This theorem is referenced by:  ralun  4152  raldifeq  4448  ralprgf  4653  ralprg  4655  raltpg  4657  ralunsn  4852  disjxun  5098  naddunif  8633  undifixp  8886  ixpfi2  9264  dffi3  9348  fseqenlem1  9948  hashf1lem1  14392  pfxsuffeqwrdeq  14635  rexfiuz  15285  modfsummods  15730  modfsummod  15731  coprmproddvdslem  16603  prmind2  16626  prmreclem2  16859  lubun  18452  efgsp1  19683  unocv  21652  coe1fzgsumdlem  22264  evl1gsumdlem  22317  basdif0  22914  isclo  23048  ordtrest2  23165  ptbasfi  23542  ptcnplem  23582  ptrescn  23600  ordthmeolem  23762  prdsxmetlem  24329  prdsbl  24452  iblcnlem1  25762  ellimc2  25851  rlimcnp  26948  xrlimcnp  26951  ftalem3  27058  dchreq  27242  2sqlem10  27412  dchrisum0flb  27494  pntpbnd1  27570  addsuniflem  28014  mulsuniflem  28162  pw2cut2  28475  elreno2  28508  wlkp1lem8  29770  pthdlem1  29857  crctcshwlkn0lem7  29907  wwlksnext  29984  clwwlkccatlem  30082  clwwlkel  30139  clwwlkwwlksb  30147  wwlksext2clwwlk  30150  clwwlknonex2lem2  30201  3wlkdlem4  30255  3pthdlem1  30257  upgr4cycl4dv4e  30278  dfconngr1  30281  cntzun  33179  ordtrest2NEW  34107  subfacp1lem3  35404  subfacp1lem5  35406  erdszelem8  35420  hfext  36405  bj-raldifsn  37380  finixpnum  37885  lindsadd  37893  lindsenlbs  37895  poimirlem26  37926  poimirlem27  37927  poimirlem32  37932  prdsbnd  38073  rrnequiv  38115  hdmap14lem13  42285  usgrexmpl1lem  48410  usgrexmpl2lem  48415  usgrexmpl2trifr  48426