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

Theorem rexlimdvv 2837
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 2830 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2831 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 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  rexlimdvva  2838  f1oiso2  6030  omeu  7012  xpdom2  7394  elfiun  7668  rankxplim3  8076  brdom6disj  8687  fpwwe2lem12  8795  tskxpss  8926  genpss  9160  genpcd  9162  genpnmax  9163  distrlem1pr  9181  distrlem5pr  9183  ltexprlem6  9197  reclem4pr  9206  supmullem1  10283  supmullem2  10284  qaddcl  10956  qmulcl  10958  sqrlem6  12720  caubnd  12829  summo  13177  xpnnenOLD  13474  bezoutlem3  13706  bezoutlem4  13707  dvdsgcd  13709  gcddiv  13715  pceu  13895  pcqcl  13905  lspfixed  17130  lspexch  17131  lsmcv  17143  lspsolvlem  17144  hausnei2  18798  uncmp  18847  txcnp  19034  tx1stc  19064  fbasrn  19298  rnelfmlem  19366  blssps  19840  blss  19841  tgqioo  20218  ovolunlem2  20822  ax5seg  23006  axpasch  23009  axeuclid  23031  pjhthmo  24527  shmodsi  24614  pjpjpre  24644  chscllem4  24865  sumdmdlem  25644  cdj3lem2a  25662  cdj3lem2b  25663  cdj3lem3a  25665  dya2iocnrect  26549  fprb  27430  btwndiff  27904  btwnconn1lem13  27976  btwnconn1lem14  27977  brsegle  27985  segletr  27991  segleantisym  27992  supadd  28259  ismblfin  28273  nn0prpwlem  28358  heibor1lem  28549  crngohomfo  28647  mzpcompact2lem  28930  pellex  29018  frgrawopreg  30485  lsmsat  32223  3dim1  32681  3dim3  32683  1cvratex  32687  atcvrlln2  32733  atcvrlln  32734  lplnnlelln  32757  llncvrlpln2  32771  lplnexllnN  32778  2llnjN  32781  lvolnlelln  32798  lvolnlelpln  32799  lplncvrlvol2  32829  2lplnj  32834  lneq2at  32992  lnatexN  32993  lncvrat  32996  lncmp  32997  paddasslem15  33048  paddasslem16  33049  pmodlem2  33061  pmapjoin  33066  llnexchb2  33083  lhp2lt  33215  cdlemf  33777  cdlemg1cex  33802  cdlemg2ce  33806  cdlemn11pre  34425  dihord2pre  34440  dihord4  34473  dihmeetlem20N  34541  mapdpglem24  34919  mapdpglem32  34920  baerlem3lem2  34925  baerlem5alem2  34926  baerlem5blem2  34927  hdmapglem7  35147
  Copyright terms: Public domain W3C validator