Theorem ceqsexv 3084

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

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1444   E.wex 1663   e. wcel 1887   _Vcvv 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-v 3047

This theorem is referenced by:  ceqsexv2d  3085  ceqsex3v  3088  gencbvex  3092  sbhypf  3095  euxfr2  3223  inuni  4565  eqvinop  4686  dfid3  4750  opeliunxp  4886  elvvv  4894  imai  5180  coi1  5351  dmfco  5939  fndmdif  5986  fndmin  5989  fmptco  6056  abrexco  6149  uniuni  6600  elxp4  6737  elxp5  6738  opabex3d  6771  opabex3  6772  fsplit  6901  brtpos2  6979  mapsnen  7647  xpsnen  7656  xpcomco  7662  xpassen  7666  dfac5lem1  8554  dfac5lem2  8555  dfac5lem3  8556  cf0  8681  ltexprlem4  9464  pceu  14796  4sqlem12  14900  vdwapun  14924  gsumval3eu  17538  dprd2d2  17677  znleval  19125  metrest  21539  fmptcof2  28259  fpwrelmapffslem  28317  dfdm5  30418  dfrn5  30419  elima4  30421  nofulllem5  30595  brtxp  30647  brpprod  30652  elfix  30670  dffix2  30672  sscoid  30680  elfuns  30682  dfiota3  30690  brimg  30704  brapply  30705  brsuccf  30708  funpartlem  30709  brrestrict  30716  dfrecs2  30717  dfrdg4  30718  lshpsmreu  32675  isopos  32746  islpln5  33100  islvol5  33144  pmapglb  33335  polval2N  33471  cdlemftr3  34132  dibelval3  34715  dicelval3  34748  mapdpglem3  35243  hdmapglem7a  35498  diophrex  35618  mapsnend  37480  opeliun2xp  40167