Theorem oprabbii

Description: Equivalent wff's yield equal operation class abstractions. (Contributed by NM, 28-May-1995) (Revised by David Abernethy, 19-Jun-2012)

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

Proof

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