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 = ( ~~ " _om )

Proof

Step Hyp Ref Expression
1 ensymb
 |-  ( x ~~ y <-> y ~~ x )
2 1 rexbii
 |-  ( E. y e. _om x ~~ y <-> E. y e. _om y ~~ x )
3 2 abbii
 |-  { x | E. y e. _om x ~~ y } = { x | E. y e. _om y ~~ x }
4 df-fin
 |-  Fin = { x | E. y e. _om x ~~ y }
5 dfima2
 |-  ( ~~ " _om ) = { x | E. y e. _om y ~~ x }
6 3 4 5 3eqtr4i
 |-  Fin = ( ~~ " _om )