Description: Alternate definition of the function relation predicate, cf. dfdisjALTV5 . (Contributed by Peter Mazsa, 5-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dffunALTV5 | |- ( FunALTV F <-> ( A. x e. ran F A. y e. ran F ( x = y \/ ( [ x ] `' F i^i [ y ] `' F ) = (/) ) /\ Rel F ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dffunALTV2 | |- ( FunALTV F <-> ( ,~ F C_ _I /\ Rel F ) ) |
|
2 | cossssid5 | |- ( ,~ F C_ _I <-> A. x e. ran F A. y e. ran F ( x = y \/ ( [ x ] `' F i^i [ y ] `' F ) = (/) ) ) |
|
3 | 2 | anbi1i | |- ( ( ,~ F C_ _I /\ Rel F ) <-> ( A. x e. ran F A. y e. ran F ( x = y \/ ( [ x ] `' F i^i [ y ] `' F ) = (/) ) /\ Rel F ) ) |
4 | 1 3 | bitri | |- ( FunALTV F <-> ( A. x e. ran F A. y e. ran F ( x = y \/ ( [ x ] `' F i^i [ y ] `' F ) = (/) ) /\ Rel F ) ) |