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 )