Theorem ceqsexv 2788

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1363   E.wex 1502   e. wcel 2158   _Vcvv 2749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-v 2751

This theorem is referenced by:  ceqsex3v  2791  gencbvex  2795  sbhypf  2798  euxfr2dc  2934  inuni  4167  eqvinop  4255  onm  4413  uniuni  4463  opeliunxp  4693  elvvv  4701  rexiunxp  4781  imai  4996  coi1  5156  abrexco  5773  opabex3d  6136  opabex3  6137  mapsnen  6825  xpsnen  6835  xpcomco  6840  xpassen  6844