Theorem ralunb 4147

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2113  ∀wral 3049   ∪ cun 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-v 3440  df-un 3904

This theorem is referenced by:  ralun  4148  raldifeq  4444  ralprgf  4649  ralprg  4651  raltpg  4653  ralunsn  4848  disjxun  5094  naddunif  8619  undifixp  8870  ixpfi2  9248  dffi3  9332  fseqenlem1  9932  hashf1lem1  14376  pfxsuffeqwrdeq  14619  rexfiuz  15269  modfsummods  15714  modfsummod  15715  coprmproddvdslem  16587  prmind2  16610  prmreclem2  16843  lubun  18436  efgsp1  19664  unocv  21633  coe1fzgsumdlem  22245  evl1gsumdlem  22298  basdif0  22895  isclo  23029  ordtrest2  23146  ptbasfi  23523  ptcnplem  23563  ptrescn  23581  ordthmeolem  23743  prdsxmetlem  24310  prdsbl  24433  iblcnlem1  25743  ellimc2  25832  rlimcnp  26929  xrlimcnp  26932  ftalem3  27039  dchreq  27223  2sqlem10  27393  dchrisum0flb  27475  pntpbnd1  27551  addsuniflem  27971  mulsuniflem  28118  pw2cut2  28419  elreno2  28440  wlkp1lem8  29701  pthdlem1  29788  crctcshwlkn0lem7  29838  wwlksnext  29915  clwwlkccatlem  30013  clwwlkel  30070  clwwlkwwlksb  30078  wwlksext2clwwlk  30081  clwwlknonex2lem2  30132  3wlkdlem4  30186  3pthdlem1  30188  upgr4cycl4dv4e  30209  dfconngr1  30212  cntzun  33110  ordtrest2NEW  34029  subfacp1lem3  35325  subfacp1lem5  35327  erdszelem8  35341  hfext  36326  bj-raldifsn  37244  finixpnum  37745  lindsadd  37753  lindsenlbs  37755  poimirlem26  37786  poimirlem27  37787  poimirlem32  37792  prdsbnd  37933  rrnequiv  37975  hdmap14lem13  42079  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2trifr  48225