Theorem ralunb 4146

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 4133	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1903	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3079	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3079	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3079	. . 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 3078   ∪ cun 3900

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-un 3907

This theorem is used by:  ralun  4147  raldifeq  4452  ralprgf  4658  ralprg  4660  raltpg  4662  ralunsn  4857  disjxun  5105  naddunif  8685  undifixp  8944  ixpfi2  9320  dffi3  9404  fseqenlem1  10030  hashf1lem1  14520  pfxsuffeqwrdeq  14767  rexfiuz  15435  modfsummods  15880  modfsummod  15881  coprmproddvdslem  16754  prmind2  16777  prmreclem2  17011  lubun  18605  efgsp1  19863  unocv  21892  lindsenlbs  22063  coe1fzgsumdlem  22527  evl1gsumdlem  22580  basdif0  23177  isclo  23311  ordtrest2  23428  ptbasfi  23806  ptcnplem  23846  ptrescn  23864  ordthmeolem  24026  prdsxmetlem  24593  prdsbl  24716  iblcnlem1  26015  ellimc2  26104  rlimcnp  27198  xrlimcnp  27201  ftalem3  27307  dchreq  27490  2sqlem10  27660  dchrisum0flb  27742  pntpbnd1  27818  addsuniflem  28262  mulsuniflem  28410  pw2cut2  28723  elreno2  28756  wlkp1lem8  30122  pthdlem1  30215  crctcshwlkn0lem7  30268  wwlksnext  30345  clwwlkccatlem  30443  clwwlkel  30500  clwwlkwwlksb  30508  wwlksext2clwwlk  30511  clwwlknonex2lem2  30562  3wlkdlem4  30626  3pthdlem1  30628  upgr4cycl4dv4e  30649  dfconngr1  30652  cntzun  33504  ordtrest2NEW  34418  subfacp1lem3  35746  subfacp1lem5  35748  erdszelem8  35762  hfext  36748  bj-raldifsn  37835  finixpnum  38344  lindsadd  38352  poimirlem26  38380  poimirlem27  38381  poimirlem32  38386  prdsbnd  38528  rrnequiv  38570  hdmap14lem13  42738  usgrexmpl1lem  48922  usgrexmpl2lem  48927  usgrexmpl2trifr  48938