Theorem ceqsexv 2776

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   E.wex 1492   e. wcel 2148   _Vcvv 2737

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739

This theorem is referenced by:  ceqsex3v  2779  gencbvex  2783  sbhypf  2786  euxfr2dc  2922  inuni  4155  eqvinop  4243  onm  4401  uniuni  4451  opeliunxp  4681  elvvv  4689  rexiunxp  4769  imai  4984  coi1  5144  abrexco  5759  opabex3d  6121  opabex3  6122  mapsnen  6810  xpsnen  6820  xpcomco  6825  xpassen  6829