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

Theorem rexlimdvv 2920
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 2912 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2914 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 1872   E.wrex 2772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-ral 2776  df-rex 2777
This theorem is referenced by:  rexlimdvva  2921  f1oiso2  6259  omeu  7298  xpdom2  7677  elfiun  7954  rankxplim3  8361  brdom6disj  8968  fpwwe2lem12  9074  tskxpss  9205  genpss  9437  genpcd  9439  genpnmax  9440  distrlem1pr  9458  distrlem5pr  9460  ltexprlem6  9474  reclem4pr  9483  supadd  10583  supmullem1  10585  supmullem2  10586  qaddcl  11288  qmulcl  11290  sqrlem6  13312  caubnd  13422  summo  13783  bezoutlem3OLD  14505  bezoutlem4OLD  14506  bezoutlem3  14508  bezoutlem4  14509  dvdsgcd  14511  gcddiv  14517  pceu  14796  pcqcl  14806  lspfixed  18351  lspexch  18352  lsmcv  18364  lspsolvlem  18365  hausnei2  20368  uncmp  20417  txcnp  20634  tx1stc  20664  fbasrn  20898  rnelfmlem  20966  blssps  21438  blss  21439  tgqioo  21817  ovolunlem2  22450  ax5seg  24967  axpasch  24970  axeuclid  24992  frgrawopreg  25776  pjhthmo  26954  shmodsi  27041  pjpjpre  27071  chscllem4  27292  sumdmdlem  28070  cdj3lem2a  28088  cdj3lem2b  28089  cdj3lem3a  28091  dya2iocnrect  29112  fprb  30421  btwndiff  30800  btwnconn1lem13  30872  btwnconn1lem14  30873  brsegle  30881  segletr  30887  segleantisym  30888  nn0prpwlem  30984  ismblfin  31946  heibor1lem  32106  crngohomfo  32204  lsmsat  32544  3dim1  33002  3dim3  33004  1cvratex  33008  atcvrlln2  33054  atcvrlln  33055  lplnnlelln  33078  llncvrlpln2  33092  lplnexllnN  33099  2llnjN  33102  lvolnlelln  33119  lvolnlelpln  33120  lplncvrlvol2  33150  2lplnj  33155  lneq2at  33313  lnatexN  33314  lncvrat  33317  lncmp  33318  paddasslem15  33369  paddasslem16  33370  pmodlem2  33382  pmapjoin  33387  llnexchb2  33404  lhp2lt  33536  cdlemf  34100  cdlemg1cex  34125  cdlemg2ce  34129  cdlemn11pre  34748  dihord2pre  34763  dihord4  34796  dihmeetlem20N  34864  mapdpglem24  35242  mapdpglem32  35243  baerlem3lem2  35248  baerlem5alem2  35249  baerlem5blem2  35250  hdmapglem7  35470  mzpcompact2lem  35563  pellex  35650  disjrnmpt2  37425  mullimc  37637  mullimcf  37644  addlimc  37670  limclner  37673  fourierdlem42  37953  fourierdlem42OLD  37954  fourierdlem80  37991  fourierdlem97  38008  sge0resplit  38157  volicorescl  38280  gbepos  38730  gbopos  38731  gbegt5  38733  gboage9  38736
  Copyright terms: Public domain W3C validator