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 ) = (/) ) } |
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 ) = (/) ) } |