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 -> y = x )

Proof

Step	Hyp	Ref	Expression
1		frege55lem2b	|- ( x = y -> [ y / z ] z = x )
2		dfsb1	|- ( [ y / z ] z = x <-> ( ( z = y -> z = x ) /\ E. z ( z = y /\ z = x ) ) )
3		eqtr2	|- ( ( z = y /\ z = x ) -> y = x )
4	3	exlimiv	|- ( E. z ( z = y /\ z = x ) -> y = x )
5	4	adantl	|- ( ( ( z = y -> z = x ) /\ E. z ( z = y /\ z = x ) ) -> y = x )
6	2 5	sylbi	|- ( [ y / z ] z = x -> y = x )
7	1 6	syl	|- ( x = y -> y = x )