Theorem ceqsexv 3118

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 1751	. 2 |- F/ x ps
2		ceqsexv.1	. 2 |- A e. _V
3		ceqsexv.2	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	ceqsex 3117	1 |- ( E. x ( x = A /\ ph ) <-> ps )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   E.wex 1659   e. wcel 1868   _Vcvv 3081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-12 1905  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-v 3083

This theorem is referenced by:  ceqsex3v  3121  gencbvex  3125  sbhypf  3128  euxfr2  3256  inuni  4583  eqvinop  4702  dfid3  4766  opeliunxp  4902  elvvv  4910  imai  5196  coi1  5367  dmfco  5952  fndmdif  5998  fndmin  6001  fmptco  6068  abrexco  6161  uniuni  6611  elxp4  6748  elxp5  6749  opabex3d  6782  opabex3  6783  fsplit  6909  brtpos2  6984  mapsnen  7651  xpsnen  7659  xpcomco  7665  xpassen  7669  dfac5lem1  8555  dfac5lem2  8556  dfac5lem3  8557  cf0  8682  ltexprlem4  9465  pceu  14784  4sqlem12  14888  vdwapun  14912  gsumval3eu  17526  dprd2d2  17665  znleval  19112  metrest  21526  ceqsexv2d  28120  fmptcof2  28249  fpwrelmapffslem  28311  dfdm5  30413  dfrn5  30414  elima4  30416  nofulllem5  30588  brtxp  30640  brpprod  30645  elfix  30663  dffix2  30665  sscoid  30673  elfuns  30675  dfiota3  30683  brimg  30697  brapply  30698  brsuccf  30701  funpartlem  30702  brrestrict  30709  dfrecs2  30710  dfrdg4  30711  lshpsmreu  32594  isopos  32665  islpln5  33019  islvol5  33063  pmapglb  33254  polval2N  33390  cdlemftr3  34051  dibelval3  34634  dicelval3  34667  mapdpglem3  35162  hdmapglem7a  35417  diophrex  35537  opeliun2xp  39388