Theorem ceqsexv 3242

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  ceqsexv2d  3243  ceqsex3v  3246  gencbvex  3250  euxfr2  3391  inuni  4826  eqvinop  4955  elvvv  5178  dmfco  6272  fndmdif  6321  fndmin  6324  fmptco  6396  abrexco  6502  uniuni  6971  elxp4  7110  elxp5  7111  opabex3d  7145  opabex3  7146  fsplit  7282  brtpos2  7358  mapsnen  8035  xpsnen  8044  xpcomco  8050  xpassen  8054  dfac5lem1  8946  dfac5lem2  8947  dfac5lem3  8948  cf0  9073  ltexprlem4  9861  pceu  15551  4sqlem12  15660  vdwapun  15678  gsumval3eu  18305  dprd2d2  18443  znleval  19903  metrest  22329  fmptcof2  29457  fpwrelmapffslem  29507  dfdm5  31676  dfrn5  31677  elima4  31679  brtxp  31987  brpprod  31992  elfix  32010  dffix2  32012  sscoid  32020  dfiota3  32030  brimg  32044  brapply  32045  brsuccf  32048  funpartlem  32049  brrestrict  32056  dfrecs2  32057  dfrdg4  32058  lshpsmreu  34396  isopos  34467  islpln5  34821  islvol5  34865  pmapglb  35056  polval2N  35192  cdlemftr3  35853  dibelval3  36436  dicelval3  36469  mapdpglem3  36964  hdmapglem7a  37219  diophrex  37339  mapsnend  39391  opeliun2xp  42111