Theorem ralunb 4138

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 4125	. . . 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 3888

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 3432  df-un 3895

This theorem is referenced by:  ralun  4139  raldifeq  4434  ralprgf  4639  ralprg  4641  raltpg  4643  ralunsn  4838  disjxun  5084  naddunif  8624  undifixp  8877  ixpfi2  9255  dffi3  9339  fseqenlem1  9941  hashf1lem1  14412  pfxsuffeqwrdeq  14655  rexfiuz  15305  modfsummods  15751  modfsummod  15752  coprmproddvdslem  16626  prmind2  16649  prmreclem2  16883  lubun  18476  efgsp1  19707  unocv  21674  coe1fzgsumdlem  22282  evl1gsumdlem  22335  basdif0  22932  isclo  23066  ordtrest2  23183  ptbasfi  23560  ptcnplem  23600  ptrescn  23618  ordthmeolem  23780  prdsxmetlem  24347  prdsbl  24470  iblcnlem1  25769  ellimc2  25858  rlimcnp  26946  xrlimcnp  26949  ftalem3  27056  dchreq  27239  2sqlem10  27409  dchrisum0flb  27491  pntpbnd1  27567  addsuniflem  28011  mulsuniflem  28159  pw2cut2  28472  elreno2  28505  wlkp1lem8  29766  pthdlem1  29853  crctcshwlkn0lem7  29903  wwlksnext  29980  clwwlkccatlem  30078  clwwlkel  30135  clwwlkwwlksb  30143  wwlksext2clwwlk  30146  clwwlknonex2lem2  30197  3wlkdlem4  30251  3pthdlem1  30253  upgr4cycl4dv4e  30274  dfconngr1  30277  cntzun  33159  ordtrest2NEW  34087  subfacp1lem3  35384  subfacp1lem5  35386  erdszelem8  35400  hfext  36385  bj-raldifsn  37432  finixpnum  37944  lindsadd  37952  lindsenlbs  37954  poimirlem26  37985  poimirlem27  37986  poimirlem32  37991  prdsbnd  38132  rrnequiv  38174  hdmap14lem13  42344  usgrexmpl1lem  48513  usgrexmpl2lem  48518  usgrexmpl2trifr  48529