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

Theorem ceqsexv 3132
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
Hypotheses
Ref Expression
ceqsexv.1  |-  A  e. 
_V
ceqsexv.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ceqsexv  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem ceqsexv
StepHypRef Expression
1 nfv 1694 . 2  |-  F/ x ps
2 ceqsexv.1 . 2  |-  A  e. 
_V
3 ceqsexv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsex 3131 1  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383   E.wex 1599    e. wcel 1804   _Vcvv 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-v 3097
This theorem is referenced by:  ceqsex3v  3135  gencbvex  3139  sbhypf  3142  euxfr2  3270  inuni  4599  eqvinop  4721  dfid3  4786  opeliunxp  5041  elvvv  5049  imai  5339  coi1  5513  dmfco  5932  fndmdif  5976  fndmin  5979  fmptco  6049  abrexco  6141  uniuni  6594  elxp4  6729  elxp5  6730  opabex3d  6763  opabex3  6764  fsplit  6890  brtpos2  6963  mapsnen  7595  xpsnen  7603  xpcomco  7609  xpassen  7613  dfac5lem1  8507  dfac5lem2  8508  dfac5lem3  8509  cf0  8634  ltexprlem4  9420  pceu  14352  4sqlem12  14456  vdwapun  14474  gsumval3eu  16886  dprd2d2  17072  znleval  18571  metrest  21005  ceqsexv2d  27375  fmptcof2  27480  fpwrelmapffslem  27533  dfdm5  29182  dfrn5  29183  elima4  29185  nofulllem5  29442  brtxp  29506  brpprod  29511  elfix  29529  dffix2  29531  sscoid  29539  elfuns  29541  dfiota3  29549  brimg  29563  brapply  29564  brsuccf  29567  funpartlem  29568  brrestrict  29575  dfrdg4  29576  tfrqfree  29577  diophrex  30685  opeliun2xp  32790  lshpsmreu  34709  isopos  34780  islpln5  35134  islvol5  35178  pmapglb  35369  polval2N  35505  cdlemftr3  36166  dibelval3  36749  dicelval3  36782  mapdpglem3  37277  hdmapglem7a  37532
  Copyright terms: Public domain W3C validator