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

Theorem rexlimdvv 2686
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 426 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2679 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2680 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  rexlimdvva  2687  f1oiso2  5865  omeu  6599  xpdom2  6973  elfiun  7199  rankxplim3  7567  brdom6disj  8173  fpwwe2lem12  8279  tskxpss  8410  genpss  8644  genpcd  8646  genpnmax  8647  distrlem1pr  8665  distrlem5pr  8667  ltexprlem6  8681  reclem4pr  8690  supmullem1  9736  supmullem2  9737  qaddcl  10348  qmulcl  10350  sqrlem6  11749  caubnd  11858  summo  12206  xpnnenOLD  12504  bezoutlem3  12735  bezoutlem4  12736  dvdsgcd  12738  gcddiv  12744  pceu  12915  pcqcl  12925  lspfixed  15897  lspexch  15898  lsmcv  15910  lspsolvlem  15911  hausnei2  17097  uncmp  17146  txcnp  17330  tx1stc  17360  fbasrn  17595  rnelfmlem  17663  blss  17988  tgqioo  18322  ovolunlem2  18873  pjhthmo  21897  shmodsi  21984  pjpjpre  22014  chscllem4  22235  sumdmdlem  23014  cdj3lem2a  23032  cdj3lem2b  23033  cdj3lem3a  23035  xrofsup  23270  fprb  24200  ax5seg  24638  axpasch  24641  axeuclid  24663  btwndiff  24722  btwnconn1lem13  24794  btwnconn1lem14  24795  brsegle  24803  segletr  24809  segleantisym  24810  supadd  24996  nn0prpwlem  26341  heibor1lem  26636  crngohomfo  26734  mzpcompact2lem  26932  pellex  27023  stoweidlem49  27901  lsmsat  29820  3dim1  30278  3dim3  30280  1cvratex  30284  atcvrlln2  30330  atcvrlln  30331  lplnnlelln  30354  llncvrlpln2  30368  lplnexllnN  30375  2llnjN  30378  lvolnlelln  30395  lvolnlelpln  30396  lplncvrlvol2  30426  2lplnj  30431  lneq2at  30589  lnatexN  30590  lncvrat  30593  lncmp  30594  paddasslem15  30645  paddasslem16  30646  pmodlem2  30658  pmapjoin  30663  llnexchb2  30680  lhp2lt  30812  cdlemf  31374  cdlemg1cex  31399  cdlemg2ce  31403  cdlemn11pre  32022  dihord2pre  32037  dihord4  32070  dihmeetlem20N  32138  mapdpglem24  32516  mapdpglem32  32517  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  hdmapglem7  32744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator