Theorem ralunb 4198

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 4185	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1903	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3081	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 640	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 306	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2147  ∀wral 3080   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-un 4154

This theorem is used by:  ralun  4199  raldifeq  4452  ralprgf  4655  ralprg  4657  raltpg  4659  ralunsn  4828  disjxun  5104  naddunif  8728  undifixp  8987  ixpfi2  9364  dffi3  9447  fseqenlem1  10127  hashf1lem1  14624  pfxsuffeqwrdeq  14872  rexfiuz  15541  modfsummods  15986  modfsummod  15987  coprmproddvdslem  16863  prmind2  16886  prmreclem2  17121  lubun  18715  efgsp1  19978  unocv  22013  lindsenlbs  22184  coe1fzgsumdlem  22648  evl1gsumdlem  22701  basdif0  23298  isclo  23432  ordtrest2  23549  ptbasfi  23927  ptcnplem  23967  ptrescn  23985  ordthmeolem  24147  prdsxmetlem  24714  prdsbl  24837  iblcnlem1  26135  ellimc2  26224  rlimcnp  27320  xrlimcnp  27323  ftalem3  27429  dchreq  27612  2sqlem10  27782  dchrisum0flb  27864  pntpbnd1  27940  addsuniflem  28414  mulsuniflem  28562  pw2cut2  28875  elreno2  28908  wlkp1lem8  30286  pthdlem1  30379  crctcshwlkn0lem7  30432  wwlksnext  30509  clwwlkccatlem  30607  clwwlkel  30664  clwwlkwwlksb  30672  wwlksext2clwwlk  30675  clwwlknonex2lem2  30726  3wlkdlem4  30790  3pthdlem1  30792  upgr4cycl4dv4e  30813  dfconngr1  30816  cntzun  33707  ordtrest2NEW  34622  subfacp1lem3  36113  subfacp1lem5  36115  erdszelem8  36129  hfext  37111  bj-raldifsn  38211  finixpnum  38719  lindsadd  38727  poimirlem26  38755  poimirlem27  38756  poimirlem32  38761  prdsbnd  38918  rrnequiv  38960  hdmap14lem13  43128  usgrexmpl1lem  49322  usgrexmpl2lem  49327  usgrexmpl2trifr  49338