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 x y y x
2 1 rexbii y ω x y y ω y x
3 2 abbii x | y ω x y = x | y ω y x
4 df-fin Fin = x | y ω x y
5 dfima2 ω = x | y ω y x
6 3 4 5 3eqtr4i Fin = ω