Theorem opabbii

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

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

Proof

Step	Hyp	Ref	Expression
1		opabbii.1	⊢ ( 𝜑 ↔ 𝜓 )
2		eqid	⊢ 𝑧 = 𝑧
3	1	a1i	⊢ ( 𝑧 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
4	3	opabbidv	⊢ ( 𝑧 = 𝑧 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
5	2 4	ax-mp	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 }