# Metamath Proof Explorer

## 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}↔\left(\left({z}={y}\to {z}={x}\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\left({z}={y}\wedge {z}={x}\right)\to {y}={x}$
5 4 adantl ${⊢}\left(\left({z}={y}\to {z}={x}\right)\wedge \exists {z}\phantom{\rule{.4em}{0ex}}\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}$