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

Theorem eximdv 1610
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 1605 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1577 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1530
This theorem is referenced by:  2eximdv  1612  exlimdv  1666  ax12olem2  1871  moim  2191  morimv  2193  reximdv2  2654  cgsexg  2821  spc3egv  2874  euind  2954  ssel  3176  reupick  3454  reximdva0  3468  uniss  3850  eusvnfb  4532  reusv2lem3  4539  reusv6OLD  4547  coss1  4841  coss2  4842  dmss  4880  dmcosseq  4948  funssres  5296  brprcneu  5520  fv3  5543  dffv2  5594  dffo4  5678  dffo5  5679  fvclss  5762  f1eqcocnv  5807  mapsn  6811  enp1i  7095  en2  7096  en4  7098  marypha2  7194  brwdom3  7298  isinffi  7627  infpwfien  7691  infmap2  7846  cfub  7877  cflm  7878  cff1  7886  cfss  7893  isf32lem9  7989  axcc4  8067  acncc  8068  domtriomlem  8070  ac6s  8113  iundom2g  8164  winalim2  8320  grudomon  8441  nsmallnq  8603  prnmadd  8623  ltexprlem1  8662  ltexprlem3  8664  ltexprlem4  8665  reclem2pr  8674  xrsupsslem  10627  xrinfmsslem  10628  supcvg  12316  vdwlem2  13031  ram0  13071  mreexexlem2d  13549  acsmapd  14283  acsmap2d  14284  dirge  14361  odcau  14917  ablfac2  15326  lspprat  15908  cmpsub  17129  cmpcld  17131  2ndcsep  17187  1stcelcls  17189  txcn  17322  fgcl  17575  ufildom1  17623  bcthlem5  18752  mbfi1flim  19080  itg2seq  19099  dchrisumlem3  20642  ubthlem1  21451  axhcompl-zf  21580  isch3  21823  cnlnssadj  22662  insiga  23500  erdsze2lem1  23736  umgraex  23877  dedekind  24084  fundmpss  24124  isconcl6a  26114  fdc1  26467  prdstotbnd  26529  prter2  26760  dfac11  27171  fnchoice  27711  rfcnnnub  27718  stoweidlem14  27774  stoweidlem27  27787  stoweidlem35  27795  stoweidlem39  27799  stoweidlem50  27810  stoweidlem53  27813  stoweidlem56  27816  stoweidlem59  27819  stoweidlem60  27820  funressnfv  28002  a9e2ndeq  28381  bnj605  29012  bnj607  29021  bnj1018  29067  lsat0cv  29296  pmapglb2N  30033  elpaddn0  30062  cdlemftr3  30827  dibglbN  31429  dihglbcpreN  31563  dihjatcclem4  31684  mapdordlem2  31900
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605
This theorem depends on definitions:  df-bi 177  df-ex 1531
  Copyright terms: Public domain W3C validator