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

Theorem eximdv 1632
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 1626 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1598 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1550
This theorem is referenced by:  2eximdv  1634  exlimdv  1646  ax12olem2OLD  2012  moim  2326  morimv  2328  reximdv2  2807  cgsexg  2979  spc3egv  3032  euind  3113  ssel  3334  reupick  3617  reximdva0  3631  uniss  4028  eusvnfb  4711  reusv2lem3  4718  reusv6OLD  4726  coss1  5020  coss2  5021  dmss  5061  dmcosseq  5129  funssres  5485  brprcneu  5713  fv3  5736  dffv2  5788  dffo4  5877  dffo5  5878  fvclss  5972  f1eqcocnv  6020  mapsn  7047  enp1i  7335  en2  7336  en4  7338  marypha2  7436  brwdom3  7542  isinffi  7871  infpwfien  7935  infmap2  8090  cfub  8121  cflm  8122  cff1  8130  cfss  8137  isf32lem9  8233  axcc4  8311  acncc  8312  domtriomlem  8314  ac6s  8356  iundom2g  8407  winalim2  8563  grudomon  8684  nsmallnq  8846  prnmadd  8866  ltexprlem1  8905  ltexprlem3  8907  ltexprlem4  8908  reclem2pr  8917  xrsupsslem  10877  xrinfmsslem  10878  supcvg  12627  vdwlem2  13342  ram0  13382  mreexexlem2d  13862  acsmapd  14596  acsmap2d  14597  dirge  14674  odcau  15230  ablfac2  15639  lspprat  16217  cmpsub  17455  cmpcld  17457  2ndcsep  17514  1stcelcls  17516  txcn  17650  fgcl  17902  ufildom1  17950  metustexhalfOLD  18585  metustexhalf  18586  bcthlem5  19273  mbfi1flim  19607  itg2seq  19626  dchrisumlem3  21177  umgraex  21350  usgraedg4  21398  ubthlem1  22364  axhcompl-zf  22493  isch3  22736  cnlnssadj  23575  ishashinf  24151  insiga  24512  erdsze2lem1  24881  dedekind  25179  fundmpss  25382  fdc1  26441  prdstotbnd  26494  prter2  26721  dfac11  27128  fnchoice  27667  rfcnnnub  27674  stoweidlem14  27730  stoweidlem27  27743  stoweidlem35  27751  stoweidlem39  27755  stoweidlem50  27766  stoweidlem56  27772  stoweidlem59  27775  stoweidlem60  27776  funressnfv  27959  frisusgranb  28324  frgrancvvdeqlemC  28365  a9e2ndeq  28583  bnj605  29215  bnj607  29224  bnj1018  29270  ax12olem2wAUX7  29393  ax12olem2OLD7  29643  lsat0cv  29768  pmapglb2N  30505  elpaddn0  30534  cdlemftr3  31299  dibglbN  31901  dihglbcpreN  32035  dihjatcclem4  32156  mapdordlem2  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator