Theorem cbvopabvOLD

Description: Obsolete version of cbvopabv as of 15-Oct-2024. (Contributed by NM, 15-Oct-1996) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cbvopabvOLD.1	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
Assertion	cbvopabvOLD	|- { <. x , y >. | ph } = { <. z , w >. | ps }

Proof

Step	Hyp	Ref	Expression
1		cbvopabvOLD.1	|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )
2		nfv	|- F/ z ph
3		nfv	|- F/ w ph
4		nfv	|- F/ x ps
5		nfv	|- F/ y ps
6	2 3 4 5 1	cbvopab	|- { <. x , y >. | ph } = { <. z , w >. | ps }