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

Theorem rexlimdvv 3189
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 441 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 3182 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 3183 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2148  wrex 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994
This theorem depends on definitions:  df-bi 198  df-an 384  df-ex 1856  df-ral 3069  df-rex 3070
This theorem is referenced by:  rexlimdvva  3190  f1oiso2  6764  omeu  7840  xpdom2  8232  elfiun  8513  rankxplim3  8929  brdom6disj  9577  fpwwe2lem12  9686  tskxpss  9817  genpss  10049  genpcd  10051  genpnmax  10052  distrlem1pr  10070  distrlem5pr  10072  ltexprlem6  10086  reclem4pr  10095  supadd  11214  supmullem1  11216  supmullem2  11217  qaddcl  12029  qmulcl  12031  sqrlem6  14218  caubnd  14328  summo  14678  bezoutlem3  15487  bezoutlem4  15488  dvdsgcd  15490  gcddiv  15497  pceu  15778  pcqcl  15788  lspfixed  19361  lspfixedOLD  19362  lspexch  19363  lsmcv  19375  lspsolvlem  19376  hausnei2  21398  uncmp  21447  txcnp  21664  tx1stc  21694  fbasrn  21928  rnelfmlem  21996  blssps  22469  blss  22470  tgqioo  22843  ovolunlem2  23506  ax5seg  26060  axpasch  26063  axeuclid  26085  upgredg2vtx  26279  pjhthmo  28518  shmodsi  28605  pjpjpre  28635  chscllem4  28856  sumdmdlem  29634  cdj3lem2a  29652  cdj3lem2b  29653  cdj3lem3a  29655  dya2iocnrect  30700  fprb  32024  btwndiff  32488  btwnconn1lem13  32560  btwnconn1lem14  32561  brsegle  32569  segletr  32575  segleantisym  32576  nn0prpwlem  32671  ismblfin  33800  heibor1lem  33956  crngohomfo  34153  lsmsat  34832  3dim1  35291  3dim3  35293  1cvratex  35297  atcvrlln2  35343  atcvrlln  35344  lplnnlelln  35367  llncvrlpln2  35381  lplnexllnN  35388  2llnjN  35391  lvolnlelln  35408  lvolnlelpln  35409  lplncvrlvol2  35439  2lplnj  35444  lneq2at  35602  lnatexN  35603  lncvrat  35606  lncmp  35607  paddasslem15  35658  paddasslem16  35659  pmodlem2  35671  pmapjoin  35676  llnexchb2  35693  lhp2lt  35825  cdlemf  36388  cdlemg1cex  36413  cdlemg2ce  36417  cdlemn11pre  37035  dihord2pre  37050  dihord4  37083  dihmeetlem20N  37151  mapdpglem24  37529  mapdpglem32  37530  baerlem3lem2  37535  baerlem5alem2  37536  baerlem5blem2  37537  hdmapglem7  37754  mzpcompact2lem  37855  pellex  37940  disjrnmpt2  39906  mullimc  40372  mullimcf  40379  addlimc  40404  limclner  40407  fourierdlem42  40889  fourierdlem80  40926  fourierdlem97  40943  sge0resplit  41146  volicorescl  41293  opnvonmbllem2  41373  smfaddlem1  41497  smflimlem6  41510  gbepos  42198  gbowpos  42199  gbegt5  42201  gboge9  42204
  Copyright terms: Public domain W3C validator