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

Step	Hyp	Ref	Expression
1		nfv 1694	. 2 |- F/ x ps
2		ceqsexv.1	. 2 |- A e. _V
3		ceqsexv.2	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	ceqsex 3131	1 |- ( E. x ( x = A /\ ph ) <-> ps )

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