Theorem cbvabvOLD

Description: Obsolete version of cbvabv as of 9-May-2023. (Contributed by NM, 26-May-1999) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	cbvabvOLD.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvabvOLD	$$⊢\left\{x|\phi \right\}=\left\{y|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		cbvabvOLD.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		nfv	$$⊢Ⅎy\phi$$
3		nfv	$$⊢Ⅎx\psi$$
4	2 3 1	cbvab	$$⊢\left\{x|\phi \right\}=\left\{y|\psi \right\}$$