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

Metamath Proof Explorer

Theorem abbi1sn

Description: Originally part of uniabio . Convert a theorem about df-iota to one about dfiota2 , without ax-10 , ax-11 , ax-12 . Although, eu6 uses ax-10 and ax-12 . (Contributed by SN, 23-Nov-2024)

		Ref	Expression
	Assertion	abbi1sn	$⊢ \forall x (φ \leftrightarrow x = y) \to \{x \| φ\} = \{y\}$

Step	Hyp	Ref	Expression
1		abbi	$⊢ \forall x (φ \leftrightarrow x = y) \to \{x \| φ\} = \{x \| x = y\}$
2		df-sn	$⊢ \{y\} = \{x \| x = y\}$
3	1 2	eqtr4di	$⊢ \forall x (φ \leftrightarrow x = y) \to \{x \| φ\} = \{y\}$