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=ω

Proof

Step Hyp Ref Expression
1 ensymb xyyx
2 1 rexbii yωxyyωyx
3 2 abbii x|yωxy=x|yωyx
4 df-fin Fin=x|yωxy
5 dfima2 ω=x|yωyx
6 3 4 5 3eqtr4i Fin=ω