Theorem ralunb 4143

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 4130	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1903	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3077	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3077	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3077	. . 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 2145  ∀wral 3076   ∪ cun 3897

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-un 3904

This theorem is used by:  ralun  4144  raldifeq  4449  ralprgf  4655  ralprg  4657  raltpg  4659  ralunsn  4854  disjxun  5101  naddunif  8689  undifixp  8948  ixpfi2  9324  dffi3  9408  fseqenlem1  10052  hashf1lem1  14545  pfxsuffeqwrdeq  14792  rexfiuz  15460  modfsummods  15905  modfsummod  15906  coprmproddvdslem  16777  prmind2  16800  prmreclem2  17034  lubun  18628  efgsp1  19890  unocv  21925  lindsenlbs  22096  coe1fzgsumdlem  22560  evl1gsumdlem  22613  basdif0  23210  isclo  23344  ordtrest2  23461  ptbasfi  23839  ptcnplem  23879  ptrescn  23897  ordthmeolem  24059  prdsxmetlem  24626  prdsbl  24749  iblcnlem1  26047  ellimc2  26136  rlimcnp  27234  xrlimcnp  27237  ftalem3  27343  dchreq  27526  2sqlem10  27696  dchrisum0flb  27778  pntpbnd1  27854  addsuniflem  28298  mulsuniflem  28446  pw2cut2  28759  elreno2  28792  wlkp1lem8  30170  pthdlem1  30263  crctcshwlkn0lem7  30316  wwlksnext  30393  clwwlkccatlem  30491  clwwlkel  30548  clwwlkwwlksb  30556  wwlksext2clwwlk  30559  clwwlknonex2lem2  30610  3wlkdlem4  30674  3pthdlem1  30676  upgr4cycl4dv4e  30697  dfconngr1  30700  cntzun  33551  ordtrest2NEW  34466  subfacp1lem3  35844  subfacp1lem5  35846  erdszelem8  35860  hfext  36832  bj-raldifsn  37917  finixpnum  38424  lindsadd  38432  poimirlem26  38460  poimirlem27  38461  poimirlem32  38466  prdsbnd  38608  rrnequiv  38650  hdmap14lem13  42818  usgrexmpl1lem  49002  usgrexmpl2lem  49007  usgrexmpl2trifr  49018