Theorem ralunb 4129

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 4116	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1827	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1878	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 277	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3056	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3056	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3056	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 635	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 305	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397  ∀wal 1546   ∈ wcel 2121  ∀wral 3055   ∪ cun 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-v 3435  df-un 3890

This theorem is referenced by:  ralun  4130  raldifeq  4424  ralprgf  4629  ralprg  4631  raltpg  4633  ralunsn  4828  disjxun  5073  naddunif  8623  undifixp  8876  ixpfi2  9254  dffi3  9338  fseqenlem1  9941  hashf1lem1  14412  pfxsuffeqwrdeq  14655  rexfiuz  15305  modfsummods  15751  modfsummod  15752  coprmproddvdslem  16626  prmind2  16649  prmreclem2  16883  lubun  18476  efgsp1  19707  unocv  21659  coe1fzgsumdlem  22293  evl1gsumdlem  22346  basdif0  22940  isclo  23074  ordtrest2  23191  ptbasfi  23568  ptcnplem  23608  ptrescn  23626  ordthmeolem  23788  prdsxmetlem  24355  prdsbl  24478  iblcnlem1  25777  ellimc2  25866  rlimcnp  26951  xrlimcnp  26954  ftalem3  27060  dchreq  27243  2sqlem10  27413  dchrisum0flb  27495  pntpbnd1  27571  addsuniflem  28015  mulsuniflem  28163  pw2cut2  28476  elreno2  28509  wlkp1lem8  29769  pthdlem1  29856  crctcshwlkn0lem7  29906  wwlksnext  29983  clwwlkccatlem  30081  clwwlkel  30138  clwwlkwwlksb  30146  wwlksext2clwwlk  30149  clwwlknonex2lem2  30200  3wlkdlem4  30254  3pthdlem1  30256  upgr4cycl4dv4e  30277  dfconngr1  30280  cntzun  33164  ordtrest2NEW  34119  subfacp1lem3  35425  subfacp1lem5  35427  erdszelem8  35441  hfext  36426  bj-raldifsn  37473  finixpnum  37987  lindsadd  37995  lindsenlbs  37997  poimirlem26  38028  poimirlem27  38029  poimirlem32  38034  prdsbnd  38175  rrnequiv  38217  hdmap14lem13  42387  usgrexmpl1lem  48526  usgrexmpl2lem  48531  usgrexmpl2trifr  48542