Theorem sbequ

Description: Equality property for substitution, from Tarski's system. Used in proof of Theorem 9.7 in Megill p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993) Revise df-sb . (Revised by BJ, 30-Dec-2020)

	Ref	Expression
Assertion	sbequ	$$⊢x=y\to \left(\left[x/z\right]\phi \leftrightarrow \left[y/z\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		equequ2	$$⊢x=y\to \left(u=x\leftrightarrow u=y\right)$$
2	1	imbi1d	$$⊢x=y\to \left(\left(u=x\to \forall z\left(z=u\to \phi \right)\right)\leftrightarrow \left(u=y\to \forall z\left(z=u\to \phi \right)\right)\right)$$
3	2	albidv	$$⊢x=y\to \left(\forall u\left(u=x\to \forall z\left(z=u\to \phi \right)\right)\leftrightarrow \forall u\left(u=y\to \forall z\left(z=u\to \phi \right)\right)\right)$$
4		df-sb	$$⊢\left[x/z\right]\phi \leftrightarrow \forall u\left(u=x\to \forall z\left(z=u\to \phi \right)\right)$$
5		df-sb	$$⊢\left[y/z\right]\phi \leftrightarrow \forall u\left(u=y\to \forall z\left(z=u\to \phi \right)\right)$$
6	3 4 5	3bitr4g	$$⊢x=y\to \left(\left[x/z\right]\phi \leftrightarrow \left[y/z\right]\phi \right)$$