Theorem ceqsexv 3021

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   E.wex 1586   e. wcel 1756   _Vcvv 2984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2986

This theorem is referenced by:  ceqsex3v  3024  gencbvex  3028  sbhypf  3031  euxfr2  3156  inuni  4466  eqvinop  4587  dfid3  4649  opeliunxp  4902  elvvv  4910  imai  5193  coi1  5365  dmfco  5777  fndmdif  5819  fndmin  5822  fmptco  5888  abrexco  5973  uniuni  6397  elxp4  6534  elxp5  6535  opabex3d  6567  opabex3  6568  fsplit  6689  brtpos2  6763  mapsnen  7399  xpsnen  7407  xpcomco  7413  xpassen  7417  dfac5lem1  8305  dfac5lem2  8306  dfac5lem3  8307  cf0  8432  ltexprlem4  9220  pceu  13925  4sqlem12  14029  vdwapun  14047  gsumval3eu  16393  dprd2d2  16555  znleval  17999  metrest  20111  ceqsexv2d  25894  fmptcof2  25991  dfdm5  27599  dfrn5  27600  elima4  27602  nofulllem5  27859  brtxp  27923  brpprod  27928  elfix  27946  dffix2  27948  sscoid  27956  elfuns  27958  dfiota3  27966  brimg  27980  brapply  27981  brsuccf  27984  funpartlem  27985  brrestrict  27992  dfrdg4  27993  tfrqfree  27994  diophrex  29126  opeliun2xp  30732  lshpsmreu  32766  isopos  32837  islpln5  33191  islvol5  33235  pmapglb  33426  polval2N  33562  cdlemftr3  34221  dibelval3  34804  dicelval3  34837  mapdpglem3  35332  hdmapglem7a  35587