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

Theorem rexlimdvv 3232
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 442 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 3225 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 3226 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2157  wrex 3104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3108  df-rex 3109
This theorem is referenced by:  rexlimdvva  3233  f1oiso2  6829  omeu  7905  xpdom2  8297  elfiun  8578  rankxplim3  8994  brdom6disj  9642  fpwwe2lem12  9751  tskxpss  9882  genpss  10114  genpcd  10116  genpnmax  10117  distrlem1pr  10135  distrlem5pr  10137  ltexprlem6  10151  reclem4pr  10160  supadd  11279  supmullem1  11281  supmullem2  11282  qaddcl  12026  qmulcl  12028  sqrlem6  14214  caubnd  14324  summo  14674  bezoutlem3  15480  bezoutlem4  15481  dvdsgcd  15483  gcddiv  15490  pceu  15771  pcqcl  15781  lspfixed  19338  lspfixedOLD  19339  lspexch  19340  lsmcv  19352  lspsolvlem  19353  hausnei2  21375  uncmp  21424  txcnp  21641  tx1stc  21671  fbasrn  21905  rnelfmlem  21973  blssps  22446  blss  22447  tgqioo  22820  ovolunlem2  23485  ax5seg  26038  axpasch  26041  axeuclid  26063  upgredg2vtx  26257  pjhthmo  28495  shmodsi  28582  pjpjpre  28612  chscllem4  28833  sumdmdlem  29611  cdj3lem2a  29629  cdj3lem2b  29630  cdj3lem3a  29632  dya2iocnrect  30674  fprb  31996  btwndiff  32460  btwnconn1lem13  32532  btwnconn1lem14  32533  brsegle  32541  segletr  32547  segleantisym  32548  nn0prpwlem  32643  ismblfin  33765  heibor1lem  33921  crngohomfo  34118  lsmsat  34790  3dim1  35249  3dim3  35251  1cvratex  35255  atcvrlln2  35301  atcvrlln  35302  lplnnlelln  35325  llncvrlpln2  35339  lplnexllnN  35346  2llnjN  35349  lvolnlelln  35366  lvolnlelpln  35367  lplncvrlvol2  35397  2lplnj  35402  lneq2at  35560  lnatexN  35561  lncvrat  35564  lncmp  35565  paddasslem15  35616  paddasslem16  35617  pmodlem2  35629  pmapjoin  35634  llnexchb2  35651  lhp2lt  35783  cdlemf  36345  cdlemg1cex  36370  cdlemg2ce  36374  cdlemn11pre  36992  dihord2pre  37007  dihord4  37040  dihmeetlem20N  37108  mapdpglem24  37486  mapdpglem32  37487  baerlem3lem2  37492  baerlem5alem2  37493  baerlem5blem2  37494  hdmapglem7  37711  mzpcompact2lem  37817  pellex  37902  disjrnmpt2  39865  mullimc  40329  mullimcf  40336  addlimc  40361  limclner  40364  fourierdlem42  40846  fourierdlem80  40883  fourierdlem97  40900  sge0resplit  41103  volicorescl  41250  opnvonmbllem2  41330  smfaddlem1  41454  smflimlem6  41467  gbepos  42222  gbowpos  42223  gbegt5  42225  gboge9  42228
  Copyright terms: Public domain W3C validator