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  1664  ax12olem2  1869  moim  2189  morimv  2191  reximdv2  2652  cgsexg  2819  spc3egv  2872  euind  2952  ssel  3174  reupick  3452  reximdva0  3466  uniss  3848  eusvnfb  4530  reusv2lem3  4537  reusv6OLD  4545  coss1  4839  coss2  4840  dmss  4878  dmcosseq  4946  funssres  5294  brprcneu  5518  fv3  5541  dffv2  5592  dffo4  5676  dffo5  5677  fvclss  5760  f1eqcocnv  5805  mapsn  6809  enp1i  7093  en2  7094  en4  7096  marypha2  7192  brwdom3  7296  isinffi  7625  infpwfien  7689  infmap2  7844  cfub  7875  cflm  7876  cff1  7884  cfss  7891  isf32lem9  7987  axcc4  8065  acncc  8066  domtriomlem  8068  ac6s  8111  iundom2g  8162  winalim2  8318  grudomon  8439  nsmallnq  8601  prnmadd  8621  ltexprlem1  8660  ltexprlem3  8662  ltexprlem4  8663  reclem2pr  8672  xrsupsslem  10625  xrinfmsslem  10626  supcvg  12314  vdwlem2  13029  ram0  13069  mreexexlem2d  13547  acsmapd  14281  acsmap2d  14282  dirge  14359  odcau  14915  ablfac2  15324  lspprat  15906  cmpsub  17127  cmpcld  17129  2ndcsep  17185  1stcelcls  17187  txcn  17320  fgcl  17573  ufildom1  17621  bcthlem5  18750  mbfi1flim  19078  itg2seq  19097  dchrisumlem3  20640  ubthlem1  21449  axhcompl-zf  21578  isch3  21821  cnlnssadj  22660  insiga  23498  erdsze2lem1  23734  umgraex  23875  dedekind  24082  fundmpss  24122  isconcl6a  26103  fdc1  26456  prdstotbnd  26518  prter2  26749  dfac11  27160  fnchoice  27700  rfcnnnub  27707  stoweidlem14  27763  stoweidlem27  27776  stoweidlem35  27784  stoweidlem39  27788  stoweidlem50  27799  stoweidlem53  27802  stoweidlem56  27805  stoweidlem59  27808  stoweidlem60  27809  funressnfv  27991  a9e2ndeq  28325  bnj605  28939  bnj607  28948  bnj1018  28994  lsat0cv  29223  pmapglb2N  29960  elpaddn0  29989  cdlemftr3  30754  dibglbN  31356  dihglbcpreN  31490  dihjatcclem4  31611  mapdordlem2  31827
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