Metamath Proof Explorer


Theorem dffunsALTV5

Description: Alternate definition of the class of functions. (Contributed by Peter Mazsa, 31-Aug-2021)

Ref Expression
Assertion dffunsALTV5
|- FunsALTV = { f e. Rels | A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) }

Proof

Step Hyp Ref Expression
1 dffunsALTV4
 |-  FunsALTV = { f e. Rels | A. u E* x u f x }
2 ineccnvmo2
 |-  ( A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) <-> A. u E* x u f x )
3 2 rabbii
 |-  { f e. Rels | A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) } = { f e. Rels | A. u E* x u f x }
4 1 3 eqtr4i
 |-  FunsALTV = { f e. Rels | A. x e. ran f A. y e. ran f ( x = y \/ ( [ x ] `' f i^i [ y ] `' f ) = (/) ) }