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

Theorem rexlimdvv 3066
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)
Hypothesis
Ref Expression
rexlimdvv.1 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
Assertion
Ref Expression
rexlimdvv (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvv
StepHypRef Expression
1 rexlimdvv.1 . . . 4 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
21expdimp 452 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 3059 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 3060 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  rexlimdvva  3067  f1oiso2  6642  omeu  7710  xpdom2  8096  elfiun  8377  rankxplim3  8782  brdom6disj  9392  fpwwe2lem12  9501  tskxpss  9632  genpss  9864  genpcd  9866  genpnmax  9867  distrlem1pr  9885  distrlem5pr  9887  ltexprlem6  9901  reclem4pr  9910  supadd  11029  supmullem1  11031  supmullem2  11032  qaddcl  11842  qmulcl  11844  sqrlem6  14032  caubnd  14142  summo  14492  bezoutlem3  15305  bezoutlem4  15306  dvdsgcd  15308  gcddiv  15315  pceu  15598  pcqcl  15608  lspfixed  19176  lspexch  19177  lsmcv  19189  lspsolvlem  19190  hausnei2  21205  uncmp  21254  txcnp  21471  tx1stc  21501  fbasrn  21735  rnelfmlem  21803  blssps  22276  blss  22277  tgqioo  22650  ovolunlem2  23312  ax5seg  25863  axpasch  25866  axeuclid  25888  upgredg2vtx  26081  pjhthmo  28289  shmodsi  28376  pjpjpre  28406  chscllem4  28627  sumdmdlem  29405  cdj3lem2a  29423  cdj3lem2b  29424  cdj3lem3a  29426  dya2iocnrect  30471  fprb  31795  btwndiff  32259  btwnconn1lem13  32331  btwnconn1lem14  32332  brsegle  32340  segletr  32346  segleantisym  32347  nn0prpwlem  32442  ismblfin  33580  heibor1lem  33738  crngohomfo  33935  lsmsat  34613  3dim1  35071  3dim3  35073  1cvratex  35077  atcvrlln2  35123  atcvrlln  35124  lplnnlelln  35147  llncvrlpln2  35161  lplnexllnN  35168  2llnjN  35171  lvolnlelln  35188  lvolnlelpln  35189  lplncvrlvol2  35219  2lplnj  35224  lneq2at  35382  lnatexN  35383  lncvrat  35386  lncmp  35387  paddasslem15  35438  paddasslem16  35439  pmodlem2  35451  pmapjoin  35456  llnexchb2  35473  lhp2lt  35605  cdlemf  36168  cdlemg1cex  36193  cdlemg2ce  36197  cdlemn11pre  36816  dihord2pre  36831  dihord4  36864  dihmeetlem20N  36932  mapdpglem24  37310  mapdpglem32  37311  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  hdmapglem7  37538  mzpcompact2lem  37631  pellex  37716  disjrnmpt2  39689  mullimc  40166  mullimcf  40173  addlimc  40198  limclner  40201  fourierdlem42  40684  fourierdlem80  40721  fourierdlem97  40738  sge0resplit  40941  volicorescl  41088  opnvonmbllem2  41168  smfaddlem1  41292  smflimlem6  41305  gbepos  41971  gbowpos  41972  gbegt5  41974  gboge9  41977
  Copyright terms: Public domain W3C validator