Theorem frege55b

Description: Lemma for frege57b . Proposition 55 of Frege1879 p. 50.

Note that eqtr2 incorporates eqcom which is stronger than this proposition which is identical to equcomi . Is it possible that Frege tricked himself into assuming what he was out to prove? (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege55b	$$⊢x=y\to y=x$$

Proof

Step	Hyp	Ref	Expression
1		frege55lem2b	$$⊢x=y\to \left[y/z\right]z=x$$
2		dfsb1	$$⊢\left[y/z\right]z=x\leftrightarrow \left(\left(z=y\to z=x\right)\wedge \exists z\left(z=y\wedge z=x\right)\right)$$
3		eqtr2	$$⊢\left(z=y\wedge z=x\right)\to y=x$$
4	3	exlimiv	$$⊢\exists z\left(z=y\wedge z=x\right)\to y=x$$
5	4	adantl	$$⊢\left(\left(z=y\to z=x\right)\wedge \exists z\left(z=y\wedge z=x\right)\right)\to y=x$$
6	2 5	sylbi	$$⊢\left[y/z\right]z=x\to y=x$$
7	1 6	syl	$$⊢x=y\to y=x$$