Theorem ceqsex

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995) (Revised by Mario Carneiro, 10-Oct-2016) (Proof shortened by Wolf Lammen, 22-Jan-2025)

	Ref	Expression
Hypotheses	ceqsex.1	|- F/ x ps
	ceqsex.2	|- A e. _V
	ceqsex.3	|- ( x = A -> ( ph <-> ps ) )
Assertion	ceqsex	|- ( E. x ( x = A /\ ph ) <-> ps )

Proof

Step	Hyp	Ref	Expression
1		ceqsex.1	|- F/ x ps
2		ceqsex.2	|- A e. _V
3		ceqsex.3	|- ( x = A -> ( ph <-> ps ) )
4		alinexa	|- ( A. x ( x = A -> -. ph ) <-> -. E. x ( x = A /\ ph ) )
5	1	nfn	|- F/ x -. ps
6	3	notbid	|- ( x = A -> ( -. ph <-> -. ps ) )
7	5 2 6	ceqsal	|- ( A. x ( x = A -> -. ph ) <-> -. ps )
8	4 7	bitr3i	|- ( -. E. x ( x = A /\ ph ) <-> -. ps )
9	8	con4bii	|- ( E. x ( x = A /\ ph ) <-> ps )