Metamath Proof Explorer


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 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }