MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralunb Structured version   Visualization version   GIF version

Theorem ralunb 4197
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
StepHypRef Expression
1 elunant 4184 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
21albii 1819 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ ∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)))
3 19.26 1870 . . 3 (∀𝑥((𝑥𝐴𝜑) ∧ (𝑥𝐵𝜑)) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
42, 3bitri 275 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
5 df-ral 3062 . 2 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝜑))
6 df-ral 3062 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
7 df-ral 3062 . . 3 (∀𝑥𝐵 𝜑 ↔ ∀𝑥(𝑥𝐵𝜑))
86, 7anbi12i 628 . 2 ((∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑) ↔ (∀𝑥(𝑥𝐴𝜑) ∧ ∀𝑥(𝑥𝐵𝜑)))
94, 5, 83bitr4i 303 1 (∀𝑥 ∈ (𝐴𝐵)𝜑 ↔ (∀𝑥𝐴 𝜑 ∧ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  wcel 2108  wral 3061  cun 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-un 3956
This theorem is referenced by:  ralun  4198  raldifeq  4494  ralprgf  4694  ralprg  4696  raltpg  4698  ralunsn  4894  disjxun  5141  naddunif  8731  undifixp  8974  ixpfi2  9390  dffi3  9471  fseqenlem1  10064  hashf1lem1  14494  pfxsuffeqwrdeq  14736  rexfiuz  15386  modfsummods  15829  modfsummod  15830  coprmproddvdslem  16699  prmind2  16722  prmreclem2  16955  lubun  18560  efgsp1  19755  unocv  21698  coe1fzgsumdlem  22307  evl1gsumdlem  22360  basdif0  22960  isclo  23095  ordtrest2  23212  ptbasfi  23589  ptcnplem  23629  ptrescn  23647  ordthmeolem  23809  prdsxmetlem  24378  prdsbl  24504  iblcnlem1  25823  ellimc2  25912  rlimcnp  27008  xrlimcnp  27011  ftalem3  27118  dchreq  27302  2sqlem10  27472  dchrisum0flb  27554  pntpbnd1  27630  addsuniflem  28034  mulsuniflem  28175  wlkp1lem8  29698  pthdlem1  29786  crctcshwlkn0lem7  29836  wwlksnext  29913  clwwlkccatlem  30008  clwwlkel  30065  clwwlkwwlksb  30073  wwlksext2clwwlk  30076  clwwlknonex2lem2  30127  3wlkdlem4  30181  3pthdlem1  30183  upgr4cycl4dv4e  30204  dfconngr1  30207  cntzun  33071  ordtrest2NEW  33922  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem8  35203  hfext  36184  bj-raldifsn  37101  finixpnum  37612  lindsadd  37620  lindsenlbs  37622  poimirlem26  37653  poimirlem27  37654  poimirlem32  37659  prdsbnd  37800  rrnequiv  37842  hdmap14lem13  41882  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2trifr  47996
  Copyright terms: Public domain W3C validator