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

Theorem rexlimdvv 2828
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 427 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2821 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2822 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  rexlimdvva  2829  f1oiso2  6064  omeu  6820  xpdom2  7195  elfiun  7427  rankxplim3  7797  brdom6disj  8402  fpwwe2lem12  8508  tskxpss  8639  genpss  8873  genpcd  8875  genpnmax  8876  distrlem1pr  8894  distrlem5pr  8896  ltexprlem6  8910  reclem4pr  8919  supmullem1  9966  supmullem2  9967  qaddcl  10582  qmulcl  10584  sqrlem6  12045  caubnd  12154  summo  12503  xpnnenOLD  12801  bezoutlem3  13032  bezoutlem4  13033  dvdsgcd  13035  gcddiv  13041  pceu  13212  pcqcl  13222  lspfixed  16192  lspexch  16193  lsmcv  16205  lspsolvlem  16206  hausnei2  17409  uncmp  17458  txcnp  17644  tx1stc  17674  fbasrn  17908  rnelfmlem  17976  blssps  18446  blss  18447  tgqioo  18823  ovolunlem2  19386  pjhthmo  22796  shmodsi  22883  pjpjpre  22913  chscllem4  23134  sumdmdlem  23913  cdj3lem2a  23931  cdj3lem2b  23932  cdj3lem3a  23934  dya2iocnrect  24623  fprb  25389  ax5seg  25869  axpasch  25872  axeuclid  25894  btwndiff  25953  btwnconn1lem13  26025  btwnconn1lem14  26026  brsegle  26034  segletr  26040  segleantisym  26041  supadd  26229  ismblfin  26237  nn0prpwlem  26316  heibor1lem  26509  crngohomfo  26607  mzpcompact2lem  26799  pellex  26889  frgrawopreg  28375  lsmsat  29743  3dim1  30201  3dim3  30203  1cvratex  30207  atcvrlln2  30253  atcvrlln  30254  lplnnlelln  30277  llncvrlpln2  30291  lplnexllnN  30298  2llnjN  30301  lvolnlelln  30318  lvolnlelpln  30319  lplncvrlvol2  30349  2lplnj  30354  lneq2at  30512  lnatexN  30513  lncvrat  30516  lncmp  30517  paddasslem15  30568  paddasslem16  30569  pmodlem2  30581  pmapjoin  30586  llnexchb2  30603  lhp2lt  30735  cdlemf  31297  cdlemg1cex  31322  cdlemg2ce  31326  cdlemn11pre  31945  dihord2pre  31960  dihord4  31993  dihmeetlem20N  32061  mapdpglem24  32439  mapdpglem32  32440  baerlem3lem2  32445  baerlem5alem2  32446  baerlem5blem2  32447  hdmapglem7  32667
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator