Theorem ralunb 4137

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 4124	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1872	. . 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 629	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 303	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3051   ∪ cun 3887

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-un 3894

This theorem is referenced by:  ralun  4138  raldifeq  4433  ralprgf  4638  ralprg  4640  raltpg  4642  ralunsn  4837  disjxun  5083  naddunif  8629  undifixp  8882  ixpfi2  9260  dffi3  9344  fseqenlem1  9946  hashf1lem1  14417  pfxsuffeqwrdeq  14660  rexfiuz  15310  modfsummods  15756  modfsummod  15757  coprmproddvdslem  16631  prmind2  16654  prmreclem2  16888  lubun  18481  efgsp1  19712  unocv  21660  coe1fzgsumdlem  22268  evl1gsumdlem  22321  basdif0  22918  isclo  23052  ordtrest2  23169  ptbasfi  23546  ptcnplem  23586  ptrescn  23604  ordthmeolem  23766  prdsxmetlem  24333  prdsbl  24456  iblcnlem1  25755  ellimc2  25844  rlimcnp  26929  xrlimcnp  26932  ftalem3  27038  dchreq  27221  2sqlem10  27391  dchrisum0flb  27473  pntpbnd1  27549  addsuniflem  27993  mulsuniflem  28141  pw2cut2  28454  elreno2  28487  wlkp1lem8  29747  pthdlem1  29834  crctcshwlkn0lem7  29884  wwlksnext  29961  clwwlkccatlem  30059  clwwlkel  30116  clwwlkwwlksb  30124  wwlksext2clwwlk  30127  clwwlknonex2lem2  30178  3wlkdlem4  30232  3pthdlem1  30234  upgr4cycl4dv4e  30255  dfconngr1  30258  cntzun  33140  ordtrest2NEW  34067  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem8  35380  hfext  36365  bj-raldifsn  37412  finixpnum  37926  lindsadd  37934  lindsenlbs  37936  poimirlem26  37967  poimirlem27  37968  poimirlem32  37973  prdsbnd  38114  rrnequiv  38156  hdmap14lem13  42326  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2trifr  48513