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

Metamath Proof Explorer

Theorem dffin1-5

Description: Compact quantifier-free version of the standard definition df-fin . (Contributed by Stefan O'Rear, 6-Jan-2015)

		Ref	Expression
	Assertion	dffin1-5	$⊢ Fin = \approx [ω]$

Step	Hyp	Ref	Expression
1		ensymb	$⊢ x \approx y \leftrightarrow y \approx x$
2	1	rexbii	$⊢ \exists y \in ω x \approx y \leftrightarrow \exists y \in ω y \approx x$
3	2	abbii	$⊢ \{x \| \exists y \in ω x \approx y\} = \{x \| \exists y \in ω y \approx x\}$
4		df-fin	$⊢ Fin = \{x \| \exists y \in ω x \approx y\}$
5		dfima2	$⊢ \approx [ω] = \{x \| \exists y \in ω y \approx x\}$
6	3 4 5	3eqtr4i	$⊢ Fin = \approx [ω]$