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 I Rel F

Proof

Step Hyp Ref Expression
1 df-funALTV FunALTV F CnvRefRel F Rel F
2 cnvrefrelcoss2 CnvRefRel F F I
3 2 anbi1i CnvRefRel F Rel F F I Rel F
4 1 3 bitri FunALTV F F I Rel F