Theorem opabbii

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

	Ref	Expression
Hypothesis	opabbii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	opabbii	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\psi \right\}$$

Proof

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