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

Theorem eximdv 1608
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
eximdv  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem eximdv
StepHypRef Expression
1 ax-17 1603 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1575 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1528
This theorem is referenced by:  2eximdv  1610  exlimdv  1665  ax12olem2  1871  moim  2190  morimv  2192  reximdv2  2653  cgsexg  2820  spc3egv  2873  euind  2953  ssel  3175  reupick  3453  reximdva0  3467  uniss  3849  eusvnfb  4529  reusv2lem3  4536  reusv6OLD  4544  coss1  4838  coss2  4839  dmss  4877  dmcosseq  4945  funssres  5260  fv3  5502  dffv2  5554  dffo4  5638  dffo5  5639  fvclss  5722  f1eqcocnv  5767  mapsn  6805  enp1i  7089  en2  7090  en4  7092  marypha2  7188  brwdom3  7292  isinffi  7621  infpwfien  7685  infmap2  7840  cfub  7871  cflm  7872  cff1  7880  cfss  7887  isf32lem9  7983  axcc4  8061  acncc  8062  domtriomlem  8064  ac6s  8107  iundom2g  8158  winalim2  8314  grudomon  8435  nsmallnq  8597  prnmadd  8617  ltexprlem1  8656  ltexprlem3  8658  ltexprlem4  8659  reclem2pr  8668  xrsupsslem  10621  xrinfmsslem  10622  supcvg  12310  vdwlem2  13025  ram0  13065  mreexexlem2d  13543  acsmapd  14277  acsmap2d  14278  dirge  14355  odcau  14911  ablfac2  15320  lspprat  15902  cmpsub  17123  cmpcld  17125  2ndcsep  17181  1stcelcls  17183  txcn  17316  fgcl  17569  ufildom1  17617  bcthlem5  18746  mbfi1flim  19074  itg2seq  19093  dchrisumlem3  20636  ubthlem1  21443  axhcompl-zf  21574  isch3  21817  cnlnssadj  22656  erdsze2lem1  23141  umgraex  23282  dedekind  23488  fundmpss  23526  isconcl6a  25514  fdc1  25867  prdstotbnd  25929  prter2  26160  dfac11  26571  fnchoice  27111  rfcnnnub  27118  stoweidlem14  27174  stoweidlem27  27187  stoweidlem35  27195  stoweidlem39  27199  stoweidlem50  27210  stoweidlem53  27213  stoweidlem56  27216  stoweidlem59  27219  stoweidlem60  27220  funressnfv  27382  a9e2ndeq  27608  bnj605  28218  bnj607  28227  bnj1018  28273  lsat0cv  28502  pmapglb2N  29239  elpaddn0  29268  cdlemftr3  30033  dibglbN  30635  dihglbcpreN  30769  dihjatcclem4  30890  mapdordlem2  31106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator