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

Theorem rexlimdvv 2961
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 437 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2953 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2955 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  rexlimdvva  2962  f1oiso2  6236  omeu  7234  xpdom2  7612  elfiun  7890  rankxplim3  8299  brdom6disj  8910  fpwwe2lem12  9019  tskxpss  9150  genpss  9382  genpcd  9384  genpnmax  9385  distrlem1pr  9403  distrlem5pr  9405  ltexprlem6  9419  reclem4pr  9428  supmullem1  10509  supmullem2  10510  qaddcl  11198  qmulcl  11200  sqrlem6  13044  caubnd  13154  summo  13502  xpnnenOLD  13804  bezoutlem3  14037  bezoutlem4  14038  dvdsgcd  14040  gcddiv  14046  pceu  14229  pcqcl  14239  lspfixed  17574  lspexch  17575  lsmcv  17587  lspsolvlem  17588  hausnei2  19648  uncmp  19697  txcnp  19884  tx1stc  19914  fbasrn  20148  rnelfmlem  20216  blssps  20690  blss  20691  tgqioo  21068  ovolunlem2  21672  ax5seg  23945  axpasch  23948  axeuclid  23970  frgrawopreg  24754  pjhthmo  25924  shmodsi  26011  pjpjpre  26041  chscllem4  26262  sumdmdlem  27041  cdj3lem2a  27059  cdj3lem2b  27060  cdj3lem3a  27062  dya2iocnrect  27920  fprb  28808  btwndiff  29282  btwnconn1lem13  29354  btwnconn1lem14  29355  brsegle  29363  segletr  29369  segleantisym  29370  supadd  29647  ismblfin  29660  nn0prpwlem  29745  heibor1lem  29936  crngohomfo  30034  mzpcompact2lem  30316  pellex  30403  mullimc  31186  mullimcf  31193  addlimc  31218  limclner  31221  fourierdlem42  31477  fourierdlem80  31515  fourierdlem97  31532  lsmsat  33823  3dim1  34281  3dim3  34283  1cvratex  34287  atcvrlln2  34333  atcvrlln  34334  lplnnlelln  34357  llncvrlpln2  34371  lplnexllnN  34378  2llnjN  34381  lvolnlelln  34398  lvolnlelpln  34399  lplncvrlvol2  34429  2lplnj  34434  lneq2at  34592  lnatexN  34593  lncvrat  34596  lncmp  34597  paddasslem15  34648  paddasslem16  34649  pmodlem2  34661  pmapjoin  34666  llnexchb2  34683  lhp2lt  34815  cdlemf  35377  cdlemg1cex  35402  cdlemg2ce  35406  cdlemn11pre  36025  dihord2pre  36040  dihord4  36073  dihmeetlem20N  36141  mapdpglem24  36519  mapdpglem32  36520  baerlem3lem2  36525  baerlem5alem2  36526  baerlem5blem2  36527  hdmapglem7  36747
  Copyright terms: Public domain W3C validator