Metamath Proof Explorer


Theorem dffunALTV5

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 ) )

Proof

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 ) )