This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opabbii

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

		Ref	Expression
	Hypothesis	opabbii.1	$⊢ φ \leftrightarrow ψ$
	Assertion	opabbii	$⊢ \{⟨x, y⟩ \| φ\} = \{⟨x, y⟩ \| ψ\}$

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