Theorem opabbidv

Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995)

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

Proof

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