Metamath Proof Explorer


Theorem dffunALTV2

Description: Alternate definition of the function relation predicate, cf. dfdisjALTV2 . (Contributed by Peter Mazsa, 8-Feb-2018)

Ref Expression
Assertion dffunALTV2
|- ( FunALTV F <-> ( ,~ F C_ _I /\ Rel F ) )

Proof

Step Hyp Ref Expression
1 df-funALTV
 |-  ( FunALTV F <-> ( CnvRefRel ,~ F /\ Rel F ) )
2 cnvrefrelcoss2
 |-  ( CnvRefRel ,~ F <-> ,~ F C_ _I )
3 2 anbi1i
 |-  ( ( CnvRefRel ,~ F /\ Rel F ) <-> ( ,~ F C_ _I /\ Rel F ) )
4 1 3 bitri
 |-  ( FunALTV F <-> ( ,~ F C_ _I /\ Rel F ) )