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	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvopabvOLD	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }

Proof

Step	Hyp	Ref	Expression
1		cbvopabvOLD.1	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
2		nfv	⊢ Ⅎ 𝑧 𝜑
3		nfv	⊢ Ⅎ 𝑤 𝜑
4		nfv	⊢ Ⅎ 𝑥 𝜓
5		nfv	⊢ Ⅎ 𝑦 𝜓
6	2 3 4 5 1	cbvopab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }