Theorem ralunb 4195

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 4182	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1851	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1902	. . 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 1567   ∈ wcel 2144  ∀wral 3076   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-un 4151

This theorem is used by:  ralun  4196  raldifeq  4448  ralprgf  4654  ralprg  4656  raltpg  4658  ralunsn  4853  disjxun  5100  naddunif  8703  undifixp  8962  ixpfi2  9339  dffi3  9423  fseqenlem1  10103  hashf1lem1  14600  pfxsuffeqwrdeq  14847  rexfiuz  15515  modfsummods  15960  modfsummod  15961  coprmproddvdslem  16837  prmind2  16860  prmreclem2  17095  lubun  18689  efgsp1  19951  unocv  21986  lindsenlbs  22157  coe1fzgsumdlem  22621  evl1gsumdlem  22674  basdif0  23271  isclo  23405  ordtrest2  23522  ptbasfi  23900  ptcnplem  23940  ptrescn  23958  ordthmeolem  24120  prdsxmetlem  24687  prdsbl  24810  iblcnlem1  26108  ellimc2  26197  rlimcnp  27293  xrlimcnp  27296  ftalem3  27402  dchreq  27585  2sqlem10  27755  dchrisum0flb  27837  pntpbnd1  27913  addsuniflem  28387  mulsuniflem  28535  pw2cut2  28848  elreno2  28881  wlkp1lem8  30259  pthdlem1  30352  crctcshwlkn0lem7  30405  wwlksnext  30482  clwwlkccatlem  30580  clwwlkel  30637  clwwlkwwlksb  30645  wwlksext2clwwlk  30648  clwwlknonex2lem2  30699  3wlkdlem4  30763  3pthdlem1  30765  upgr4cycl4dv4e  30786  dfconngr1  30789  cntzun  33640  ordtrest2NEW  34555  subfacp1lem3  35947  subfacp1lem5  35949  erdszelem8  35963  hfext  36934  bj-raldifsn  38021  finixpnum  38529  lindsadd  38537  poimirlem26  38565  poimirlem27  38566  poimirlem32  38571  prdsbnd  38728  rrnequiv  38770  hdmap14lem13  42938  usgrexmpl1lem  49119  usgrexmpl2lem  49124  usgrexmpl2trifr  49135