Theorem frege55b 38191

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

Note that eqtr2 2642 incorporates eqcom 2629 which is stronger than this proposition which is identical to equcomi 1944. Is is 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	|- ( x = y -> y = x )

Proof of Theorem frege55b

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		frege55lem2b 38190	. 2 |- ( x = y -> [ y / z ] z = x )
2		df-sb 1881	. . 3 |- ( [ y / z ] z = x <-> ( ( z = y -> z = x ) /\ E. z ( z = y /\ z = x ) ) )
3		eqtr2 2642	. . . . 5 |- ( ( z = y /\ z = x ) -> y = x )
4	3	exlimiv 1858	. . . 4 |- ( E. z ( z = y /\ z = x ) -> y = x )
5	4	adantl 482	. . 3 |- ( ( ( z = y -> z = x ) /\ E. z ( z = y /\ z = x ) ) -> y = x )
6	2, 5	sylbi 207	. 2 |- ( [ y / z ] z = x -> y = x )
7	1, 6	syl 17	1 |- ( x = y -> y = x )

Syntax hints:   -> wi 4   /\ wa 384   E.wex 1704   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-13 2246  ax-ext 2602  ax-frege8 38103  ax-frege52c 38182

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  frege56b  38192