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

Theorem eximdv 1612
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 1606 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1578 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1531
This theorem is referenced by:  2eximdv  1614  exlimdv  1626  ax12olem2  1881  moim  2202  morimv  2204  reximdv2  2665  cgsexg  2832  spc3egv  2885  euind  2965  ssel  3187  reupick  3465  reximdva0  3479  uniss  3864  eusvnfb  4546  reusv2lem3  4553  reusv6OLD  4561  coss1  4855  coss2  4856  dmss  4894  dmcosseq  4962  funssres  5310  brprcneu  5534  fv3  5557  dffv2  5608  dffo4  5692  dffo5  5693  fvclss  5776  f1eqcocnv  5821  mapsn  6825  enp1i  7109  en2  7110  en4  7112  marypha2  7208  brwdom3  7312  isinffi  7641  infpwfien  7705  infmap2  7860  cfub  7891  cflm  7892  cff1  7900  cfss  7907  isf32lem9  8003  axcc4  8081  acncc  8082  domtriomlem  8084  ac6s  8127  iundom2g  8178  winalim2  8334  grudomon  8455  nsmallnq  8617  prnmadd  8637  ltexprlem1  8676  ltexprlem3  8678  ltexprlem4  8679  reclem2pr  8688  xrsupsslem  10641  xrinfmsslem  10642  supcvg  12330  vdwlem2  13045  ram0  13085  mreexexlem2d  13563  acsmapd  14297  acsmap2d  14298  dirge  14375  odcau  14931  ablfac2  15340  lspprat  15922  cmpsub  17143  cmpcld  17145  2ndcsep  17201  1stcelcls  17203  txcn  17336  fgcl  17589  ufildom1  17637  bcthlem5  18766  mbfi1flim  19094  itg2seq  19113  dchrisumlem3  20656  ubthlem1  21465  axhcompl-zf  21594  isch3  21837  cnlnssadj  22676  insiga  23513  erdsze2lem1  23749  umgraex  23890  dedekind  24097  fundmpss  24193  isconcl6a  26206  fdc1  26559  prdstotbnd  26621  prter2  26852  dfac11  27263  fnchoice  27803  rfcnnnub  27810  stoweidlem14  27866  stoweidlem27  27879  stoweidlem35  27887  stoweidlem39  27891  stoweidlem50  27902  stoweidlem53  27905  stoweidlem56  27908  stoweidlem59  27911  stoweidlem60  27912  funressnfv  28096  a9e2ndeq  28624  bnj605  29255  bnj607  29264  bnj1018  29310  ax12olem2wAUX7  29433  ax12olem2OLD7  29660  lsat0cv  29845  pmapglb2N  30582  elpaddn0  30611  cdlemftr3  31376  dibglbN  31978  dihglbcpreN  32112  dihjatcclem4  32233  mapdordlem2  32449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator