Theorem cbvoprab12v

Description: Rule used to change first two bound variables in an operation abstraction, using implicit substitution. (Contributed by NM, 8-Oct-2004)

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

Proof

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