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

Theorem eximdv 2018
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  2020  immo  2159  moimv  2161  reximdv2  2614  cgsexg  2757  cla43egv  2809  euind  2889  ssel  3097  reupick  3359  reximdva0  3373  uniss  3748  eusvnfb  4421  reusv2lem3  4428  reusv6OLD  4436  coss1  4746  coss2  4747  dmss  4785  dmcosseq  4853  funssres  5151  fv3  5393  dffv2  5444  dffo4  5528  dffo5  5529  fvclss  5612  f1eqcocnv  5657  mapsn  6695  enp1i  6978  en2  6979  en4  6981  marypha2  7076  brwdom3  7180  isinffi  7509  infpwfien  7573  infmap2  7728  cfub  7759  cflm  7760  cff1  7768  cfss  7775  isf32lem9  7871  axcc4  7949  acncc  7950  domtriomlem  7952  ac6s  7995  iundom2g  8046  winalim2  8198  grudomon  8319  nsmallnq  8481  prnmadd  8501  ltexprlem1  8540  ltexprlem3  8542  ltexprlem4  8543  reclem2pr  8552  xrsupsslem  10503  xrinfmsslem  10504  supcvg  12188  vdwlem2  12903  ram0  12943  dirge  14194  odcau  14750  ablfac2  15159  lspprat  15740  cmpsub  16959  cmpcld  16961  2ndcsep  17017  1stcelcls  17019  txcn  17152  fgcl  17405  ufildom1  17453  bcthlem5  18582  mbfi1flim  18910  itg2seq  18929  dchrisumlem3  20472  ubthlem1  21279  axhcompl-zf  21408  isch3  21651  cnlnssadj  22490  erdsze2lem1  22905  umgraex  23046  dedekind  23252  fundmpss  23290  isconcl6a  25269  fdc1  25622  prdstotbnd  25684  prter2  25915  dfac11  26326  a9e2ndeq  27018  bnj605  27628  bnj607  27637  bnj1018  27683  lsat0cv  27912  pmapglb2N  28649  elpaddn0  28678  cdlemftr3  29443  dibglbN  30045  dihglbcpreN  30179  dihjatcclem4  30300  mapdordlem2  30516
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