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

Theorem eximdv 2019
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 nfv 1629 . 2  |-  F/ x ph
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximd 1711 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6   E.wex 1537
This theorem is referenced by:  2eximdv  2021  moim  2164  morimv  2166  reximdv2  2627  cgsexg  2794  cla43egv  2847  euind  2927  ssel  3149  reupick  3427  reximdva0  3441  uniss  3822  eusvnfb  4502  reusv2lem3  4509  reusv6OLD  4517  coss1  4827  coss2  4828  dmss  4866  dmcosseq  4934  funssres  5232  fv3  5474  dffv2  5526  dffo4  5610  dffo5  5611  fvclss  5694  f1eqcocnv  5739  mapsn  6777  enp1i  7061  en2  7062  en4  7064  marypha2  7160  brwdom3  7264  isinffi  7593  infpwfien  7657  infmap2  7812  cfub  7843  cflm  7844  cff1  7852  cfss  7859  isf32lem9  7955  axcc4  8033  acncc  8034  domtriomlem  8036  ac6s  8079  iundom2g  8130  winalim2  8286  grudomon  8407  nsmallnq  8569  prnmadd  8589  ltexprlem1  8628  ltexprlem3  8630  ltexprlem4  8631  reclem2pr  8640  xrsupsslem  10592  xrinfmsslem  10593  supcvg  12277  vdwlem2  12992  ram0  13032  mreexexlem2d  13510  acsmapd  14244  acsmap2d  14245  dirge  14322  odcau  14878  ablfac2  15287  lspprat  15869  cmpsub  17090  cmpcld  17092  2ndcsep  17148  1stcelcls  17150  txcn  17283  fgcl  17536  ufildom1  17584  bcthlem5  18713  mbfi1flim  19041  itg2seq  19060  dchrisumlem3  20603  ubthlem1  21410  axhcompl-zf  21539  isch3  21782  cnlnssadj  22621  erdsze2lem1  23107  umgraex  23248  dedekind  23454  fundmpss  23492  isconcl6a  25471  fdc1  25824  prdstotbnd  25886  prter2  26117  dfac11  26528  fnchoice  27069  rfcnnnub  27076  stoweidlem14  27132  stoweidlem27  27145  stoweidlem35  27153  stoweidlem39  27157  stoweidlem50  27168  stoweidlem53  27171  stoweidlem56  27174  stoweidlem59  27177  stoweidlem60  27178  a9e2ndeq  27461  bnj605  28071  bnj607  28080  bnj1018  28126  lsat0cv  28473  pmapglb2N  29210  elpaddn0  29239  cdlemftr3  30004  dibglbN  30606  dihglbcpreN  30740  dihjatcclem4  30861  mapdordlem2  31077
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator