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

Theorem rexlimdvv 2930
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 438 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2922 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2924 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1870   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788
This theorem is referenced by:  rexlimdvva  2931  f1oiso2  6258  omeu  7294  xpdom2  7673  elfiun  7950  rankxplim3  8351  brdom6disj  8958  fpwwe2lem12  9065  tskxpss  9196  genpss  9428  genpcd  9430  genpnmax  9431  distrlem1pr  9449  distrlem5pr  9451  ltexprlem6  9465  reclem4pr  9474  supadd  10575  supmullem1  10577  supmullem2  10578  qaddcl  11280  qmulcl  11282  sqrlem6  13290  caubnd  13400  summo  13761  bezoutlem3  14479  bezoutlem4  14480  dvdsgcd  14482  gcddiv  14488  pceu  14759  pcqcl  14769  lspfixed  18286  lspexch  18287  lsmcv  18299  lspsolvlem  18300  hausnei2  20300  uncmp  20349  txcnp  20566  tx1stc  20596  fbasrn  20830  rnelfmlem  20898  blssps  21370  blss  21371  tgqioo  21729  ovolunlem2  22329  ax5seg  24814  axpasch  24817  axeuclid  24839  frgrawopreg  25622  pjhthmo  26790  shmodsi  26877  pjpjpre  26907  chscllem4  27128  sumdmdlem  27906  cdj3lem2a  27924  cdj3lem2b  27925  cdj3lem3a  27927  dya2iocnrect  28942  fprb  30200  btwndiff  30579  btwnconn1lem13  30651  btwnconn1lem14  30652  brsegle  30660  segletr  30666  segleantisym  30667  nn0prpwlem  30763  ismblfin  31685  heibor1lem  31845  crngohomfo  31943  lsmsat  32283  3dim1  32741  3dim3  32743  1cvratex  32747  atcvrlln2  32793  atcvrlln  32794  lplnnlelln  32817  llncvrlpln2  32831  lplnexllnN  32838  2llnjN  32841  lvolnlelln  32858  lvolnlelpln  32859  lplncvrlvol2  32889  2lplnj  32894  lneq2at  33052  lnatexN  33053  lncvrat  33056  lncmp  33057  paddasslem15  33108  paddasslem16  33109  pmodlem2  33121  pmapjoin  33126  llnexchb2  33143  lhp2lt  33275  cdlemf  33839  cdlemg1cex  33864  cdlemg2ce  33868  cdlemn11pre  34487  dihord2pre  34502  dihord4  34535  dihmeetlem20N  34603  mapdpglem24  34981  mapdpglem32  34982  baerlem3lem2  34987  baerlem5alem2  34988  baerlem5blem2  34989  hdmapglem7  35209  mzpcompact2lem  35302  pellex  35389  disjrnmpt2  37086  mullimc  37268  mullimcf  37275  addlimc  37301  limclner  37304  fourierdlem42  37580  fourierdlem80  37618  fourierdlem97  37635  sge0resplit  37782  gbepos  38249  gbopos  38250  gbegt5  38252  gboage9  38255
  Copyright terms: Public domain W3C validator