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

Theorem rexlimdvv 2675
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 2668 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2669 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 1686   E.wrex 2546
This theorem is referenced by:  rexlimdvva  2676  f1oiso2  5851  omeu  6585  xpdom2  6959  elfiun  7185  rankxplim3  7553  brdom6disj  8159  fpwwe2lem12  8265  tskxpss  8396  genpss  8630  genpcd  8632  genpnmax  8633  distrlem1pr  8651  distrlem5pr  8653  ltexprlem6  8667  reclem4pr  8676  supmullem1  9722  supmullem2  9723  qaddcl  10334  qmulcl  10336  sqrlem6  11735  caubnd  11844  summo  12192  xpnnenOLD  12490  bezoutlem3  12721  bezoutlem4  12722  dvdsgcd  12724  gcddiv  12730  pceu  12901  pcqcl  12911  lspfixed  15883  lspexch  15884  lsmcv  15896  lspsolvlem  15897  hausnei2  17083  uncmp  17132  txcnp  17316  tx1stc  17346  fbasrn  17581  rnelfmlem  17649  blss  17974  tgqioo  18308  ovolunlem2  18859  pjhthmo  21883  shmodsi  21970  pjpjpre  22000  chscllem4  22221  sumdmdlem  23000  cdj3lem2a  23018  cdj3lem2b  23019  cdj3lem3a  23021  xrofsup  23257  fprb  24131  ax5seg  24568  axpasch  24571  axeuclid  24593  btwndiff  24652  btwnconn1lem13  24724  btwnconn1lem14  24725  brsegle  24733  segletr  24739  segleantisym  24740  supadd  24928  nn0prpwlem  26249  heibor1lem  26544  crngohomfo  26642  mzpcompact2lem  26840  pellex  26931  stoweidlem49  27809  lsmsat  29271  3dim1  29729  3dim3  29731  1cvratex  29735  atcvrlln2  29781  atcvrlln  29782  lplnnlelln  29805  llncvrlpln2  29819  lplnexllnN  29826  2llnjN  29829  lvolnlelln  29846  lvolnlelpln  29847  lplncvrlvol2  29877  2lplnj  29882  lneq2at  30040  lnatexN  30041  lncvrat  30044  lncmp  30045  paddasslem15  30096  paddasslem16  30097  pmodlem2  30109  pmapjoin  30114  llnexchb2  30131  lhp2lt  30263  cdlemf  30825  cdlemg1cex  30850  cdlemg2ce  30854  cdlemn11pre  31473  dihord2pre  31488  dihord4  31521  dihmeetlem20N  31589  mapdpglem24  31967  mapdpglem32  31968  baerlem3lem2  31973  baerlem5alem2  31974  baerlem5blem2  31975  hdmapglem7  32195
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-nf 1534  df-ral 2550  df-rex 2551
  Copyright terms: Public domain W3C validator