Theorem frege55lem2b

Description: Lemma for frege55b . Core proof of Proposition 55 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege55lem2b	$$⊢x=y\to \left[y/z\right]z=x$$

Proof

Step	Hyp	Ref	Expression
1		frege54cor1b	$$⊢\left[x/z\right]z=x$$
2		frege53b	$$⊢\left[x/z\right]z=x\to \left(x=y\to \left[y/z\right]z=x\right)$$
3	1 2	ax-mp	$$⊢x=y\to \left[y/z\right]z=x$$