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\to A=x$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	frege54cor1c	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}y=x$$
3		frege53c	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}y=x\to \left(x=A\to \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y=x\right)$$
4	2 3	ax-mp	$$⊢x=A\to \underset{\dot{}}{[}A/y\underset{\dot{}}{]}y=x$$
5		df-sbc	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y=x\leftrightarrow A\in \left\{y|y=x\right\}$$
6		clelab	$$⊢A\in \left\{y|y=x\right\}\leftrightarrow \exists y\left(y=A\wedge y=x\right)$$
7	5 6	bitri	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y=x\leftrightarrow \exists y\left(y=A\wedge y=x\right)$$
8		eqtr2	$$⊢\left(y=A\wedge y=x\right)\to A=x$$
9	8	exlimiv	$$⊢\exists y\left(y=A\wedge y=x\right)\to A=x$$
10	7 9	sylbi	$$⊢\underset{\dot{}}{[}A/y\underset{\dot{}}{]}y=x\to A=x$$
11	4 10	syl	$$⊢x=A\to A=x$$