Theorem ralunb 4150

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 4137	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
2	1	albii 1849	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)))
3		19.26 1900	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝜑) ∧ (𝑥 ∈ 𝐵 → 𝜑)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
5		df-ral 3080	. 2 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝜑))
6		df-ral 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
7		df-ral 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
8	6, 7	anbi12i 639	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑)))
9	4, 5, 8	3bitr4i 306	1 ⊢ (∀𝑥 ∈ (𝐴 ∪ 𝐵)𝜑 ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐵 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   ∈ wcel 2143  ∀wral 3079   ∪ cun 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-un 3910

This theorem is used by:  ralun  4151  raldifeq  4454  ralprgf  4660  ralprg  4662  raltpg  4664  ralunsn  4859  disjxun  5107  naddunif  8676  undifixp  8928  ixpfi2  9303  dffi3  9387  fseqenlem1  10013  hashf1lem1  14497  pfxsuffeqwrdeq  14740  rexfiuz  15404  modfsummods  15850  modfsummod  15851  coprmproddvdslem  16724  prmind2  16747  prmreclem2  16981  lubun  18575  efgsp1  19811  unocv  21839  coe1fzgsumdlem  22472  evl1gsumdlem  22525  basdif0  23119  isclo  23253  ordtrest2  23370  ptbasfi  23747  ptcnplem  23787  ptrescn  23805  ordthmeolem  23967  prdsxmetlem  24534  prdsbl  24657  iblcnlem1  25956  ellimc2  26045  rlimcnp  27139  xrlimcnp  27142  ftalem3  27248  dchreq  27431  2sqlem10  27601  dchrisum0flb  27683  pntpbnd1  27759  addsuniflem  28203  mulsuniflem  28351  pw2cut2  28664  elreno2  28697  wlkp1lem8  30037  pthdlem1  30124  crctcshwlkn0lem7  30174  wwlksnext  30251  clwwlkccatlem  30349  clwwlkel  30406  clwwlkwwlksb  30414  wwlksext2clwwlk  30417  clwwlknonex2lem2  30468  3wlkdlem4  30522  3pthdlem1  30524  upgr4cycl4dv4e  30545  dfconngr1  30548  cntzun  33408  ordtrest2NEW  34322  subfacp1lem3  35682  subfacp1lem5  35684  erdszelem8  35698  hfext  36683  bj-raldifsn  37770  finixpnum  38284  lindsadd  38292  lindsenlbs  38294  poimirlem26  38325  poimirlem27  38326  poimirlem32  38331  prdsbnd  38472  rrnequiv  38514  hdmap14lem13  42682  usgrexmpl1lem  48814  usgrexmpl2lem  48819  usgrexmpl2trifr  48830