Theorem ceqex

Description: Equality implies equivalence with substitution. (Contributed by NM, 2-Mar-1995) (Proof shortened by BJ, 1-May-2019)

	Ref	Expression
Assertion	ceqex	|- ( x = A -> ( ph <-> E. x ( x = A /\ ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	|- ( ( x = A /\ ph ) -> E. x ( x = A /\ ph ) )
2	1	ex	|- ( x = A -> ( ph -> E. x ( x = A /\ ph ) ) )
3		eqvisset	|- ( x = A -> A e. _V )
4		alexeqg	|- ( A e. _V -> ( A. x ( x = A -> ph ) <-> E. x ( x = A /\ ph ) ) )
5	3 4	syl	|- ( x = A -> ( A. x ( x = A -> ph ) <-> E. x ( x = A /\ ph ) ) )
6		sp	|- ( A. x ( x = A -> ph ) -> ( x = A -> ph ) )
7	6	com12	|- ( x = A -> ( A. x ( x = A -> ph ) -> ph ) )
8	5 7	sylbird	|- ( x = A -> ( E. x ( x = A /\ ph ) -> ph ) )
9	2 8	impbid	|- ( x = A -> ( ph <-> E. x ( x = A /\ ph ) ) )