Theorem cbvopabv

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996)

	Ref	Expression
Hypothesis	cbvopabv.1	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvopabv	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ 𝜓 }

Proof

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