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

Theorem rexlimdvv 2749
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 2742 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2743 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 1710   E.wrex 2620
This theorem is referenced by:  rexlimdvva  2750  f1oiso2  5936  omeu  6670  xpdom2  7045  elfiun  7273  rankxplim3  7641  brdom6disj  8247  fpwwe2lem12  8353  tskxpss  8484  genpss  8718  genpcd  8720  genpnmax  8721  distrlem1pr  8739  distrlem5pr  8741  ltexprlem6  8755  reclem4pr  8764  supmullem1  9810  supmullem2  9811  qaddcl  10424  qmulcl  10426  sqrlem6  11829  caubnd  11938  summo  12287  xpnnenOLD  12585  bezoutlem3  12816  bezoutlem4  12817  dvdsgcd  12819  gcddiv  12825  pceu  12996  pcqcl  13006  lspfixed  15980  lspexch  15981  lsmcv  15993  lspsolvlem  15994  hausnei2  17187  uncmp  17236  txcnp  17420  tx1stc  17450  fbasrn  17681  rnelfmlem  17749  blss  18074  tgqioo  18408  ovolunlem2  18961  pjhthmo  21995  shmodsi  22082  pjpjpre  22112  chscllem4  22333  sumdmdlem  23112  cdj3lem2a  23130  cdj3lem2b  23131  cdj3lem3a  23133  xrofsup  23327  dya2iocnrect  23895  fprb  24687  ax5seg  25125  axpasch  25128  axeuclid  25150  btwndiff  25209  btwnconn1lem13  25281  btwnconn1lem14  25282  brsegle  25290  segletr  25296  segleantisym  25297  supadd  25483  nn0prpwlem  25562  heibor1lem  25856  crngohomfo  25954  mzpcompact2lem  26152  pellex  26243  stoweidlem49  27121  frgrawopreg  27882  lsmsat  29267  3dim1  29725  3dim3  29727  1cvratex  29731  atcvrlln2  29777  atcvrlln  29778  lplnnlelln  29801  llncvrlpln2  29815  lplnexllnN  29822  2llnjN  29825  lvolnlelln  29842  lvolnlelpln  29843  lplncvrlvol2  29873  2lplnj  29878  lneq2at  30036  lnatexN  30037  lncvrat  30040  lncmp  30041  paddasslem15  30092  paddasslem16  30093  pmodlem2  30105  pmapjoin  30110  llnexchb2  30127  lhp2lt  30259  cdlemf  30821  cdlemg1cex  30846  cdlemg2ce  30850  cdlemn11pre  31469  dihord2pre  31484  dihord4  31517  dihmeetlem20N  31585  mapdpglem24  31963  mapdpglem32  31964  baerlem3lem2  31969  baerlem5alem2  31970  baerlem5blem2  31971  hdmapglem7  32191
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2624  df-rex 2625
  Copyright terms: Public domain W3C validator