Theorem drsb2

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005)

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

Proof

Step	Hyp	Ref	Expression
1		sbequ	$$⊢x=y\to \left(\left[x/z\right]\phi \leftrightarrow \left[y/z\right]\phi \right)$$
2	1	sps	$$⊢\forall xx=y\to \left(\left[x/z\right]\phi \leftrightarrow \left[y/z\right]\phi \right)$$