Theorem ceqsexv 3150

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   _Vcvv 3113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115

This theorem is referenced by:  ceqsex3v  3153  gencbvex  3157  sbhypf  3160  euxfr2  3288  inuni  4609  eqvinop  4731  dfid3  4796  opeliunxp  5051  elvvv  5059  imai  5349  coi1  5523  dmfco  5941  fndmdif  5985  fndmin  5988  fmptco  6054  abrexco  6144  uniuni  6593  elxp4  6728  elxp5  6729  opabex3d  6762  opabex3  6763  fsplit  6888  brtpos2  6961  mapsnen  7593  xpsnen  7601  xpcomco  7607  xpassen  7611  dfac5lem1  8504  dfac5lem2  8505  dfac5lem3  8506  cf0  8631  ltexprlem4  9417  pceu  14229  4sqlem12  14333  vdwapun  14351  gsumval3eu  16710  dprd2d2  16895  znleval  18388  metrest  20790  ceqsexv2d  27101  fmptcof2  27202  dfdm5  28811  dfrn5  28812  elima4  28814  nofulllem5  29071  brtxp  29135  brpprod  29140  elfix  29158  dffix2  29160  sscoid  29168  elfuns  29170  dfiota3  29178  brimg  29192  brapply  29193  brsuccf  29196  funpartlem  29197  brrestrict  29204  dfrdg4  29205  tfrqfree  29206  diophrex  30341  opeliun2xp  32018  lshpsmreu  33924  isopos  33995  islpln5  34349  islvol5  34393  pmapglb  34584  polval2N  34720  cdlemftr3  35379  dibelval3  35962  dicelval3  35995  mapdpglem3  36490  hdmapglem7a  36745