Theorem frege55c

Description: Proposition 55 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege55c	|- ( x = A -> A = x )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	frege54cor1c	|- [. x / y ]. y = x
3		frege53c	|- ( [. x / y ]. y = x -> ( x = A -> [. A / y ]. y = x ) )
4	2 3	ax-mp	|- ( x = A -> [. A / y ]. y = x )
5		df-sbc	|- ( [. A / y ]. y = x <-> A e. { y | y = x } )
6		clelab	|- ( A e. { y | y = x } <-> E. y ( y = A /\ y = x ) )
7	5 6	bitri	|- ( [. A / y ]. y = x <-> E. y ( y = A /\ y = x ) )
8		eqtr2	|- ( ( y = A /\ y = x ) -> A = x )
9	8	exlimiv	|- ( E. y ( y = A /\ y = x ) -> A = x )
10	7 9	sylbi	|- ( [. A / y ]. y = x -> A = x )
11	4 10	syl	|- ( x = A -> A = x )