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	$$⊢\phi \leftrightarrow \psi$$
Assertion	oprabbii	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		oprabbii.1	$$⊢\phi \leftrightarrow \psi$$
2		eqid	$$⊢w=w$$
3	1	a1i	$$⊢w=w\to \left(\phi \leftrightarrow \psi \right)$$
4	3	oprabbidv	$$⊢w=w\to \left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$
5	2 4	ax-mp	$$⊢\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨⟨x,y⟩,z⟩|\psi \right\}$$