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