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

Metamath Proof Explorer

Theorem abbii

Description: Equivalent wff's yield equal class abstractions (inference form). (Contributed by NM, 26-May-1993) Remove dependency on ax-10 , ax-11 , and ax-12 . (Revised by Steven Nguyen, 3-May-2023)

		Ref	Expression
	Hypothesis	abbii.1	$⊢ φ \leftrightarrow ψ$
	Assertion	abbii	$⊢ \{x \| φ\} = \{x \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		abbii.1	$⊢ φ \leftrightarrow ψ$
2		abbi	$⊢ \forall x (φ \leftrightarrow ψ) \to \{x \| φ\} = \{x \| ψ\}$
3	2 1	mpg	$⊢ \{x \| φ\} = \{x \| ψ\}$