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

Theorem rexlimdvv 2674
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)
Hypothesis
Ref Expression
rexlimdvv.1  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimdvv  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Distinct variable groups:    x, y, ph    ch, x, y    y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem rexlimdvv
StepHypRef Expression
1 rexlimdvv.1 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ( ps  ->  ch ) ) )
21expdimp 426 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2667 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2668 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1685   E.wrex 2545
This theorem is referenced by:  rexlimdvva  2675  f1oiso2  5811  omeu  6579  xpdom2  6953  elfiun  7179  rankxplim3  7547  brdom6disj  8153  fpwwe2lem12  8259  tskxpss  8390  genpss  8624  genpcd  8626  genpnmax  8627  distrlem1pr  8645  distrlem5pr  8647  ltexprlem6  8661  reclem4pr  8670  supmullem1  9716  supmullem2  9717  qaddcl  10328  qmulcl  10330  sqrlem6  11729  caubnd  11838  summo  12186  xpnnenOLD  12484  bezoutlem3  12715  bezoutlem4  12716  dvdsgcd  12718  gcddiv  12724  pceu  12895  pcqcl  12905  lspfixed  15877  lspexch  15878  lsmcv  15890  lspsolvlem  15891  hausnei2  17077  uncmp  17126  txcnp  17310  tx1stc  17340  fbasrn  17575  rnelfmlem  17643  blss  17968  tgqioo  18302  ovolunlem2  18853  pjhthmo  21877  shmodsi  21964  pjpjpre  21994  chscllem4  22215  sumdmdlem  22994  cdj3lem2a  23012  cdj3lem2b  23013  cdj3lem3a  23015  fprb  23533  axfelem19  23768  ax5seg  23976  axpasch  23979  axeuclid  24001  btwndiff  24060  btwnconn1lem13  24132  btwnconn1lem14  24133  brsegle  24141  segletr  24147  segleantisym  24148  nn0prpwlem  25649  heibor1lem  25944  crngohomfo  26042  mzpcompact2lem  26240  pellex  26331  stoweidlem49  27209  lsmsat  28477  3dim1  28935  3dim3  28937  1cvratex  28941  atcvrlln2  28987  atcvrlln  28988  lplnnlelln  29011  llncvrlpln2  29025  lplnexllnN  29032  2llnjN  29035  lvolnlelln  29052  lvolnlelpln  29053  lplncvrlvol2  29083  2lplnj  29088  lneq2at  29246  lnatexN  29247  lncvrat  29250  lncmp  29251  paddasslem15  29302  paddasslem16  29303  pmodlem2  29315  pmapjoin  29320  llnexchb2  29337  lhp2lt  29469  cdlemf  30031  cdlemg1cex  30056  cdlemg2ce  30060  cdlemn11pre  30679  dihord2pre  30694  dihord4  30727  dihmeetlem20N  30795  mapdpglem24  31173  mapdpglem32  31174  baerlem3lem2  31179  baerlem5alem2  31180  baerlem5blem2  31181  hdmapglem7  31401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator