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

Theorem rexlimdvv 2868
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 437 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
y  e.  B  -> 
( ps  ->  ch ) ) )
32rexlimdv 2861 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps  ->  ch ) )
43rexlimdva 2862 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2741  df-rex 2742
This theorem is referenced by:  rexlimdvva  2869  f1oiso2  6064  omeu  7045  xpdom2  7427  elfiun  7701  rankxplim3  8109  brdom6disj  8720  fpwwe2lem12  8829  tskxpss  8960  genpss  9194  genpcd  9196  genpnmax  9197  distrlem1pr  9215  distrlem5pr  9217  ltexprlem6  9231  reclem4pr  9240  supmullem1  10317  supmullem2  10318  qaddcl  10990  qmulcl  10992  sqrlem6  12758  caubnd  12867  summo  13215  xpnnenOLD  13513  bezoutlem3  13745  bezoutlem4  13746  dvdsgcd  13748  gcddiv  13754  pceu  13934  pcqcl  13944  lspfixed  17231  lspexch  17232  lsmcv  17244  lspsolvlem  17245  hausnei2  18979  uncmp  19028  txcnp  19215  tx1stc  19245  fbasrn  19479  rnelfmlem  19547  blssps  20021  blss  20022  tgqioo  20399  ovolunlem2  21003  ax5seg  23206  axpasch  23209  axeuclid  23231  pjhthmo  24727  shmodsi  24814  pjpjpre  24844  chscllem4  25065  sumdmdlem  25844  cdj3lem2a  25862  cdj3lem2b  25863  cdj3lem3a  25865  dya2iocnrect  26718  fprb  27606  btwndiff  28080  btwnconn1lem13  28152  btwnconn1lem14  28153  brsegle  28161  segletr  28167  segleantisym  28168  supadd  28444  ismblfin  28458  nn0prpwlem  28543  heibor1lem  28734  crngohomfo  28832  mzpcompact2lem  29114  pellex  29202  frgrawopreg  30668  lsmsat  32749  3dim1  33207  3dim3  33209  1cvratex  33213  atcvrlln2  33259  atcvrlln  33260  lplnnlelln  33283  llncvrlpln2  33297  lplnexllnN  33304  2llnjN  33307  lvolnlelln  33324  lvolnlelpln  33325  lplncvrlvol2  33355  2lplnj  33360  lneq2at  33518  lnatexN  33519  lncvrat  33522  lncmp  33523  paddasslem15  33574  paddasslem16  33575  pmodlem2  33587  pmapjoin  33592  llnexchb2  33609  lhp2lt  33741  cdlemf  34303  cdlemg1cex  34328  cdlemg2ce  34332  cdlemn11pre  34951  dihord2pre  34966  dihord4  34999  dihmeetlem20N  35067  mapdpglem24  35445  mapdpglem32  35446  baerlem3lem2  35451  baerlem5alem2  35452  baerlem5blem2  35453  hdmapglem7  35673
  Copyright terms: Public domain W3C validator