Description: Define the function relation predicate, i.e., the function predicate. This definition of the function predicate (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun , are always the same, that is ( FunALTV F <-> Fun F ) , see funALTVfun .
The element of the class of functions and the function predicate are the same, that is ( F e. FunsALTV <-> FunALTV F ) when F is a set, see elfunsALTVfunALTV . Alternate definitions are dffunALTV2 , ... , dffunALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | df-funALTV |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cF | ||
1 | 0 | wfunALTV | |
2 | 0 | ccoss | |
3 | 2 | wcnvrefrel | |
4 | 0 | wrel | |
5 | 3 4 | wa | |
6 | 1 5 | wb |