Theorem ralunb 4172

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2108  ∀wral 3051   ∪ cun 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-un 3931

This theorem is referenced by:  ralun  4173  raldifeq  4469  ralprgf  4670  ralprg  4672  raltpg  4674  ralunsn  4870  disjxun  5117  naddunif  8705  undifixp  8948  ixpfi2  9362  dffi3  9443  fseqenlem1  10038  hashf1lem1  14473  pfxsuffeqwrdeq  14716  rexfiuz  15366  modfsummods  15809  modfsummod  15810  coprmproddvdslem  16681  prmind2  16704  prmreclem2  16937  lubun  18525  efgsp1  19718  unocv  21640  coe1fzgsumdlem  22241  evl1gsumdlem  22294  basdif0  22891  isclo  23025  ordtrest2  23142  ptbasfi  23519  ptcnplem  23559  ptrescn  23577  ordthmeolem  23739  prdsxmetlem  24307  prdsbl  24430  iblcnlem1  25741  ellimc2  25830  rlimcnp  26927  xrlimcnp  26930  ftalem3  27037  dchreq  27221  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  addsuniflem  27960  mulsuniflem  28104  wlkp1lem8  29660  pthdlem1  29748  crctcshwlkn0lem7  29798  wwlksnext  29875  clwwlkccatlem  29970  clwwlkel  30027  clwwlkwwlksb  30035  wwlksext2clwwlk  30038  clwwlknonex2lem2  30089  3wlkdlem4  30143  3pthdlem1  30145  upgr4cycl4dv4e  30166  dfconngr1  30169  cntzun  33062  ordtrest2NEW  33954  subfacp1lem3  35204  subfacp1lem5  35206  erdszelem8  35220  hfext  36201  bj-raldifsn  37118  finixpnum  37629  lindsadd  37637  lindsenlbs  37639  poimirlem26  37670  poimirlem27  37671  poimirlem32  37676  prdsbnd  37817  rrnequiv  37859  hdmap14lem13  41899  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2trifr  48041