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

Theorem rexlimdvv 2772
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 2765 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2766 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 1717   E.wrex 2643
This theorem is referenced by:  rexlimdvva  2773  f1oiso2  6004  omeu  6757  xpdom2  7132  elfiun  7363  rankxplim3  7731  brdom6disj  8336  fpwwe2lem12  8442  tskxpss  8573  genpss  8807  genpcd  8809  genpnmax  8810  distrlem1pr  8828  distrlem5pr  8830  ltexprlem6  8844  reclem4pr  8853  supmullem1  9899  supmullem2  9900  qaddcl  10515  qmulcl  10517  sqrlem6  11973  caubnd  12082  summo  12431  xpnnenOLD  12729  bezoutlem3  12960  bezoutlem4  12961  dvdsgcd  12963  gcddiv  12969  pceu  13140  pcqcl  13150  lspfixed  16120  lspexch  16121  lsmcv  16133  lspsolvlem  16134  hausnei2  17332  uncmp  17381  txcnp  17566  tx1stc  17596  fbasrn  17830  rnelfmlem  17898  blss  18339  tgqioo  18695  ovolunlem2  19254  pjhthmo  22645  shmodsi  22732  pjpjpre  22762  chscllem4  22983  sumdmdlem  23762  cdj3lem2a  23780  cdj3lem2b  23781  cdj3lem3a  23783  dya2iocnrect  24418  fprb  25146  ax5seg  25584  axpasch  25587  axeuclid  25609  btwndiff  25668  btwnconn1lem13  25740  btwnconn1lem14  25741  brsegle  25749  segletr  25755  segleantisym  25756  supadd  25941  nn0prpwlem  26009  heibor1lem  26202  crngohomfo  26300  mzpcompact2lem  26492  pellex  26582  frgrawopreg  27794  lsmsat  29174  3dim1  29632  3dim3  29634  1cvratex  29638  atcvrlln2  29684  atcvrlln  29685  lplnnlelln  29708  llncvrlpln2  29722  lplnexllnN  29729  2llnjN  29732  lvolnlelln  29749  lvolnlelpln  29750  lplncvrlvol2  29780  2lplnj  29785  lneq2at  29943  lnatexN  29944  lncvrat  29947  lncmp  29948  paddasslem15  29999  paddasslem16  30000  pmodlem2  30012  pmapjoin  30017  llnexchb2  30034  lhp2lt  30166  cdlemf  30728  cdlemg1cex  30753  cdlemg2ce  30757  cdlemn11pre  31376  dihord2pre  31391  dihord4  31424  dihmeetlem20N  31492  mapdpglem24  31870  mapdpglem32  31871  baerlem3lem2  31876  baerlem5alem2  31877  baerlem5blem2  31878  hdmapglem7  32098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2647  df-rex 2648
  Copyright terms: Public domain W3C validator