Metamath Proof Explorer


Theorem funALTVfun

Description: Our definition of the function predicate df-funALTV (based on a more general, converse reflexive, relation) and the original definition of function in set.mm df-fun , are always the same and interchangeable. (Contributed by Peter Mazsa, 27-Jul-2021)

Ref Expression
Assertion funALTVfun FunALTV F Fun F

Proof

Step Hyp Ref Expression
1 cnvrefrelcoss2 CnvRefRel F F I
2 dfcoss3 F = F F -1
3 2 sseq1i F I F F -1 I
4 1 3 bitri CnvRefRel F F F -1 I
5 4 anbi2ci CnvRefRel F Rel F Rel F F F -1 I
6 df-funALTV FunALTV F CnvRefRel F Rel F
7 df-fun Fun F Rel F F F -1 I
8 5 6 7 3bitr4i FunALTV F Fun F