Theorem ralunb 4206

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1534   ∈ wcel 2105  ∀wral 3058   ∪ cun 3960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-v 3479  df-un 3967

This theorem is referenced by:  ralun  4207  raldifeq  4499  ralprgf  4698  ralprg  4700  raltpg  4702  ralunsn  4898  disjxun  5145  naddunif  8729  undifixp  8972  ixpfi2  9387  dffi3  9468  fseqenlem1  10061  hashf1lem1  14490  pfxsuffeqwrdeq  14732  rexfiuz  15382  modfsummods  15825  modfsummod  15826  coprmproddvdslem  16695  prmind2  16718  prmreclem2  16950  lubun  18572  efgsp1  19769  unocv  21715  coe1fzgsumdlem  22322  evl1gsumdlem  22375  basdif0  22975  isclo  23110  ordtrest2  23227  ptbasfi  23604  ptcnplem  23644  ptrescn  23662  ordthmeolem  23824  prdsxmetlem  24393  prdsbl  24519  iblcnlem1  25837  ellimc2  25926  rlimcnp  27022  xrlimcnp  27025  ftalem3  27132  dchreq  27316  2sqlem10  27486  dchrisum0flb  27568  pntpbnd1  27644  addsuniflem  28048  mulsuniflem  28189  wlkp1lem8  29712  pthdlem1  29798  crctcshwlkn0lem7  29845  wwlksnext  29922  clwwlkccatlem  30017  clwwlkel  30074  clwwlkwwlksb  30082  wwlksext2clwwlk  30085  clwwlknonex2lem2  30136  3wlkdlem4  30190  3pthdlem1  30192  upgr4cycl4dv4e  30213  dfconngr1  30216  cntzun  33053  ordtrest2NEW  33883  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem8  35182  hfext  36164  bj-raldifsn  37082  finixpnum  37591  lindsadd  37599  lindsenlbs  37601  poimirlem26  37632  poimirlem27  37633  poimirlem32  37638  prdsbnd  37779  rrnequiv  37821  hdmap14lem13  41862  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2trifr  47931