Theorem oprabbidv

Description: Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004)

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

Proof

Step	Hyp	Ref	Expression
1		oprabbidv.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2		nfv	⊢ Ⅎ 𝑥 𝜑
3		nfv	⊢ Ⅎ 𝑦 𝜑
4		nfv	⊢ Ⅎ 𝑧 𝜑
5	2 3 4 1	oprabbid	⊢ ( 𝜑 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜒 } )