Theorem ceqsex

Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995) (Revised by Mario Carneiro, 10-Oct-2016)

	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	3	biimpa	|- ( ( x = A /\ ph ) -> ps )
5	1 4	exlimi	|- ( E. x ( x = A /\ ph ) -> ps )
6	3	biimprcd	|- ( ps -> ( x = A -> ph ) )
7	1 6	alrimi	|- ( ps -> A. x ( x = A -> ph ) )
8	2	isseti	|- E. x x = A
9		exintr	|- ( A. x ( x = A -> ph ) -> ( E. x x = A -> E. x ( x = A /\ ph ) ) )
10	7 8 9	mpisyl	|- ( ps -> E. x ( x = A /\ ph ) )
11	5 10	impbii	|- ( E. x ( x = A /\ ph ) <-> ps )