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  immo  2162  moimv  2164  reximdv2  2623  cgsexg  2770  cla43egv  2823  euind  2903  ssel  3116  reupick  3394  reximdva0  3408  uniss  3789  eusvnfb  4467  reusv2lem3  4474  reusv6OLD  4482  coss1  4792  coss2  4793  dmss  4831  dmcosseq  4899  funssres  5197  fv3  5439  dffv2  5491  dffo4  5575  dffo5  5576  fvclss  5659  f1eqcocnv  5704  mapsn  6742  enp1i  7026  en2  7027  en4  7029  marypha2  7125  brwdom3  7229  isinffi  7558  infpwfien  7622  infmap2  7777  cfub  7808  cflm  7809  cff1  7817  cfss  7824  isf32lem9  7920  axcc4  7998  acncc  7999  domtriomlem  8001  ac6s  8044  iundom2g  8095  winalim2  8251  grudomon  8372  nsmallnq  8534  prnmadd  8554  ltexprlem1  8593  ltexprlem3  8595  ltexprlem4  8596  reclem2pr  8605  xrsupsslem  10556  xrinfmsslem  10557  supcvg  12241  vdwlem2  12956  ram0  12996  mreexexlem2d  13474  acsmapd  14208  acsmap2d  14209  dirge  14286  odcau  14842  ablfac2  15251  lspprat  15833  cmpsub  17054  cmpcld  17056  2ndcsep  17112  1stcelcls  17114  txcn  17247  fgcl  17500  ufildom1  17548  bcthlem5  18677  mbfi1flim  19005  itg2seq  19024  dchrisumlem3  20567  ubthlem1  21374  axhcompl-zf  21503  isch3  21746  cnlnssadj  22585  erdsze2lem1  23071  umgraex  23212  dedekind  23418  fundmpss  23456  isconcl6a  25435  fdc1  25788  prdstotbnd  25850  prter2  26081  dfac11  26492  fnchoice  27033  rfcnnnub  27040  stoweidlem14  27063  stoweidlem27  27076  stoweidlem35  27084  stoweidlem39  27088  stoweidlem50  27099  stoweidlem53  27102  stoweidlem56  27105  stoweidlem59  27108  stoweidlem60  27109  a9e2ndeq  27341  bnj605  27951  bnj607  27960  bnj1018  28006  lsat0cv  28353  pmapglb2N  29090  elpaddn0  29119  cdlemftr3  29884  dibglbN  30486  dihglbcpreN  30620  dihjatcclem4  30741  mapdordlem2  30957
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