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

Theorem rexlimdvv 2673
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 2666 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2667 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 1684   E.wrex 2544
This theorem is referenced by:  rexlimdvva  2674  f1oiso2  5849  omeu  6583  xpdom2  6957  elfiun  7183  rankxplim3  7551  brdom6disj  8157  fpwwe2lem12  8263  tskxpss  8394  genpss  8628  genpcd  8630  genpnmax  8631  distrlem1pr  8649  distrlem5pr  8651  ltexprlem6  8665  reclem4pr  8674  supmullem1  9720  supmullem2  9721  qaddcl  10332  qmulcl  10334  sqrlem6  11733  caubnd  11842  summo  12190  xpnnenOLD  12488  bezoutlem3  12719  bezoutlem4  12720  dvdsgcd  12722  gcddiv  12728  pceu  12899  pcqcl  12909  lspfixed  15881  lspexch  15882  lsmcv  15894  lspsolvlem  15895  hausnei2  17081  uncmp  17130  txcnp  17314  tx1stc  17344  fbasrn  17579  rnelfmlem  17647  blss  17972  tgqioo  18306  ovolunlem2  18857  pjhthmo  21881  shmodsi  21968  pjpjpre  21998  chscllem4  22219  sumdmdlem  22998  cdj3lem2a  23016  cdj3lem2b  23017  cdj3lem3a  23019  xrofsup  23255  fprb  24129  ax5seg  24566  axpasch  24569  axeuclid  24591  btwndiff  24650  btwnconn1lem13  24722  btwnconn1lem14  24723  brsegle  24731  segletr  24737  segleantisym  24738  nn0prpwlem  26238  heibor1lem  26533  crngohomfo  26631  mzpcompact2lem  26829  pellex  26920  stoweidlem49  27798  lsmsat  29198  3dim1  29656  3dim3  29658  1cvratex  29662  atcvrlln2  29708  atcvrlln  29709  lplnnlelln  29732  llncvrlpln2  29746  lplnexllnN  29753  2llnjN  29756  lvolnlelln  29773  lvolnlelpln  29774  lplncvrlvol2  29804  2lplnj  29809  lneq2at  29967  lnatexN  29968  lncvrat  29971  lncmp  29972  paddasslem15  30023  paddasslem16  30024  pmodlem2  30036  pmapjoin  30041  llnexchb2  30058  lhp2lt  30190  cdlemf  30752  cdlemg1cex  30777  cdlemg2ce  30781  cdlemn11pre  31400  dihord2pre  31415  dihord4  31448  dihmeetlem20N  31516  mapdpglem24  31894  mapdpglem32  31895  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  hdmapglem7  32122
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 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator