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

Theorem rexlimdvv 2648
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 428 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2641 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2642 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2519
This theorem is referenced by:  rexlimdvva  2649  f1oiso2  5783  omeu  6551  xpdom2  6925  elfiun  7151  rankxplim3  7519  brdom6disj  8125  fpwwe2lem12  8231  tskxpss  8362  genpss  8596  genpcd  8598  genpnmax  8599  distrlem1pr  8617  distrlem5pr  8619  ltexprlem6  8633  reclem4pr  8642  supmullem1  9688  supmullem2  9689  qaddcl  10300  qmulcl  10302  sqrlem6  11699  caubnd  11808  summo  12156  xpnnenOLD  12451  bezoutlem3  12682  bezoutlem4  12683  dvdsgcd  12685  gcddiv  12691  pceu  12862  pcqcl  12872  lspfixed  15844  lspexch  15845  lsmcv  15857  lspsolvlem  15858  hausnei2  17044  uncmp  17093  txcnp  17277  tx1stc  17307  fbasrn  17542  rnelfmlem  17610  blss  17935  tgqioo  18269  ovolunlem2  18820  pjhthmo  21842  shmodsi  21929  pjpjpre  21959  chscllem4  22180  sumdmdlem  22959  cdj3lem2a  22977  cdj3lem2b  22978  cdj3lem3a  22980  fprb  23499  axfelem19  23734  ax5seg  23942  axpasch  23945  axeuclid  23967  btwndiff  24026  btwnconn1lem13  24098  btwnconn1lem14  24099  brsegle  24107  segletr  24113  segleantisym  24114  nn0prpwlem  25606  heibor1lem  25901  crngohomfo  25999  mzpcompact2lem  26197  pellex  26288  stoweidlem49  27167  lsmsat  28448  3dim1  28906  3dim3  28908  1cvratex  28912  atcvrlln2  28958  atcvrlln  28959  lplnnlelln  28982  llncvrlpln2  28996  lplnexllnN  29003  2llnjN  29006  lvolnlelln  29023  lvolnlelpln  29024  lplncvrlvol2  29054  2lplnj  29059  lneq2at  29217  lnatexN  29218  lncvrat  29221  lncmp  29222  paddasslem15  29273  paddasslem16  29274  pmodlem2  29286  pmapjoin  29291  llnexchb2  29308  lhp2lt  29440  cdlemf  30002  cdlemg1cex  30027  cdlemg2ce  30031  cdlemn11pre  30650  dihord2pre  30665  dihord4  30698  dihmeetlem20N  30766  mapdpglem24  31144  mapdpglem32  31145  baerlem3lem2  31150  baerlem5alem2  31151  baerlem5blem2  31152  hdmapglem7  31372
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2523  df-rex 2524
  Copyright terms: Public domain W3C validator