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

Theorem rexlimdvv 3205
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 454 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 3151 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 3153 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3075
This theorem is referenced by:  rexlimdvva  3206  fprb  7144  f1oiso2  7298  omeu  8533  xpdom2  9012  rex2dom  9191  elfiun  9367  rankxplim3  9818  brdom6disj  10469  fpwwe2lem11  10578  tskxpss  10709  genpss  10941  genpcd  10943  genpnmax  10944  distrlem1pr  10962  distrlem5pr  10964  ltexprlem6  10978  reclem4pr  10987  supadd  12124  supmullem1  12126  supmullem2  12127  qaddcl  12891  qmulcl  12893  01sqrexlem6  15133  caubnd  15244  summo  15603  bezoutlem3  16423  bezoutlem4  16424  dvdsgcd  16426  gcddiv  16433  pceu  16719  pcqcl  16729  symgpssefmnd  19178  lspfixed  20592  lspexch  20593  lsmcv  20605  lspsolvlem  20606  hausnei2  22707  uncmp  22757  txcnp  22974  tx1stc  23004  fbasrn  23238  rnelfmlem  23306  blssps  23780  blss  23781  tgqioo  24166  ovolunlem2  24865  2sqnn  26790  madebdayim  27220  ax5seg  27890  axpasch  27893  axeuclid  27915  upgredg2vtx  28095  pjhthmo  30247  shmodsi  30334  pjpjpre  30364  chscllem4  30585  sumdmdlem  31363  cdj3lem2a  31381  cdj3lem2b  31382  cdj3lem3a  31384  dya2iocnrect  32884  satffunlem2lem1  34001  btwndiff  34615  btwnconn1lem13  34687  btwnconn1lem14  34688  brsegle  34696  segletr  34702  segleantisym  34703  nn0prpwlem  34797  ismblfin  36122  heibor1lem  36271  crngohomfo  36468  lsmsat  37473  3dim1  37933  3dim3  37935  1cvratex  37939  atcvrlln2  37985  atcvrlln  37986  lplnnlelln  38009  llncvrlpln2  38023  lplnexllnN  38030  2llnjN  38033  lvolnlelln  38050  lvolnlelpln  38051  lplncvrlvol2  38081  2lplnj  38086  lneq2at  38244  lnatexN  38245  lncvrat  38248  lncmp  38249  paddasslem15  38300  paddasslem16  38301  pmodlem2  38313  pmapjoin  38318  llnexchb2  38335  lhp2lt  38467  cdlemf  39029  cdlemg1cex  39054  cdlemg2ce  39058  cdlemn11pre  39676  dihord2pre  39691  dihord4  39724  dihmeetlem20N  39792  mapdpglem24  40170  mapdpglem32  40171  baerlem3lem2  40176  baerlem5alem2  40177  baerlem5blem2  40178  hdmapglem7  40395  sn-addid2  40876  rexlimdv3d  41009  mzpcompact2lem  41077  pellex  41161  onexomgt  41578  onexoegt  41581  disjrnmpt2  43414  mullimc  43864  mullimcf  43871  addlimc  43896  limclner  43899  fourierdlem42  44397  fourierdlem80  44434  fourierdlem97  44451  sge0resplit  44654  volicorescl  44801  opnvonmbllem2  44881  smfaddlem1  45011  smflimlem6  45024  gbepos  45957  gbowpos  45958  gbegt5  45960  gboge9  45963  seposep  46965  iscnrm3lem6  46978
  Copyright terms: Public domain W3C validator