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	⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		frege55lem2b	⊢ ( 𝑥 = 𝑦 → [ 𝑦 / 𝑧 ] 𝑧 = 𝑥 )
2		dfsb1	⊢ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑥 ↔ ( ( 𝑧 = 𝑦 → 𝑧 = 𝑥 ) ∧ ∃ 𝑧 ( 𝑧 = 𝑦 ∧ 𝑧 = 𝑥 ) ) )
3		eqtr2	⊢ ( ( 𝑧 = 𝑦 ∧ 𝑧 = 𝑥 ) → 𝑦 = 𝑥 )
4	3	exlimiv	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑦 ∧ 𝑧 = 𝑥 ) → 𝑦 = 𝑥 )
5	4	adantl	⊢ ( ( ( 𝑧 = 𝑦 → 𝑧 = 𝑥 ) ∧ ∃ 𝑧 ( 𝑧 = 𝑦 ∧ 𝑧 = 𝑥 ) ) → 𝑦 = 𝑥 )
6	2 5	sylbi	⊢ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑥 → 𝑦 = 𝑥 )
7	1 6	syl	⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 )