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

Theorem rexlimdvv 2635
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 428 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2628 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2629 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   E.wrex 2510
This theorem is referenced by:  rexlimdvva  2636  f1oiso2  5701  omeu  6469  xpdom2  6842  elfiun  7067  rankxplim3  7435  brdom6disj  8041  fpwwe2lem12  8143  tskxpss  8274  genpss  8508  genpcd  8510  genpnmax  8511  distrlem1pr  8529  distrlem5pr  8531  ltexprlem6  8545  reclem4pr  8554  supmullem1  9600  supmullem2  9601  qaddcl  10211  qmulcl  10213  sqrlem6  11610  caubnd  11719  summo  12067  xpnnenOLD  12362  bezoutlem3  12593  bezoutlem4  12594  dvdsgcd  12596  gcddiv  12602  pceu  12773  pcqcl  12783  lspfixed  15716  lspexch  15717  lsmcv  15729  lspsolvlem  15730  hausnei2  16913  uncmp  16962  txcnp  17146  tx1stc  17176  fbasrn  17411  rnelfmlem  17479  blss  17804  tgqioo  18138  ovolunlem2  18689  pjhthmo  21711  shmodsi  21798  pjpjpre  21828  chscllem4  22067  sumdmdlem  22828  cdj3lem2a  22846  cdj3lem2b  22847  cdj3lem3a  22849  fprb  23297  axfelem19  23532  ax5seg  23740  axpasch  23743  axeuclid  23765  btwndiff  23824  btwnconn1lem13  23896  btwnconn1lem14  23897  brsegle  23905  segletr  23911  segleantisym  23912  nn0prpwlem  25404  heibor1lem  25699  crngohomfo  25797  mzpcompact2lem  25995  pellex  26086  lsmsat  27887  3dim1  28345  3dim3  28347  1cvratex  28351  atcvrlln2  28397  atcvrlln  28398  lplnnlelln  28421  llncvrlpln2  28435  lplnexllnN  28442  2llnjN  28445  lvolnlelln  28462  lvolnlelpln  28463  lplncvrlvol2  28493  2lplnj  28498  lneq2at  28656  lnatexN  28657  lncvrat  28660  lncmp  28661  paddasslem15  28712  paddasslem16  28713  pmodlem2  28725  pmapjoin  28730  llnexchb2  28747  lhp2lt  28879  cdlemf  29441  cdlemg1cex  29466  cdlemg2ce  29470  cdlemn11pre  30089  dihord2pre  30104  dihord4  30137  dihmeetlem20N  30205  mapdpglem24  30583  mapdpglem32  30584  baerlem3lem2  30589  baerlem5alem2  30590  baerlem5blem2  30591  hdmapglem7  30811
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator