Theorem sb2ae

Description: In the case of two successive substitutions for two always equal variables, the second substitution has no effect. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by BJ and WL, 9-Aug-2023) (New usage is discouraged.)

	Ref	Expression
Assertion	sb2ae	$$⊢\forall xx=y\to \left(\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[v/y\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		drsb1	$$⊢\forall xx=y\to \left(\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[u/y\right]\left[v/y\right]\phi \right)$$
2		nfs1v	$$⊢Ⅎy\left[v/y\right]\phi$$
3	2	sbf	$$⊢\left[u/y\right]\left[v/y\right]\phi \leftrightarrow \left[v/y\right]\phi$$
4	1 3	bitrdi	$$⊢\forall xx=y\to \left(\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[v/y\right]\phi \right)$$