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	$$⊢\mathrm{Fin}=\approx \left[\mathrm{\omega }\right]$$

Proof

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