Theorem frege55b 44080

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

Note that eqtr2 2755 incorporates eqcom 2741 which is stronger than this proposition which is identical to equcomi 2018. 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.)

Assertion

Ref	Expression
frege55b	⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Proof of Theorem frege55b

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		frege55lem2b 44079	. 2 ⊢ (𝑥 = 𝑦 → [𝑦 / 𝑧]𝑧 = 𝑥)
2		dfsb1 2483	. . 3 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 ↔ ((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)))
3		eqtr2 2755	. . . . 5 ⊢ ((𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
4	3	exlimiv 1931	. . . 4 ⊢ (∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥) → 𝑦 = 𝑥)
5	4	adantl 481	. . 3 ⊢ (((𝑧 = 𝑦 → 𝑧 = 𝑥) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 = 𝑥)) → 𝑦 = 𝑥)
6	2, 5	sylbi 217	. 2 ⊢ ([𝑦 / 𝑧]𝑧 = 𝑥 → 𝑦 = 𝑥)
7	1, 6	syl 17	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-13 2374  ax-ext 2706  ax-frege8 43992  ax-frege52c 44071

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-sbc 3739

This theorem is referenced by:  frege56b  44081