Metamath Proof Explorer


Theorem dffunsALTV2

Description: Alternate definition of the class of functions. (Contributed by Peter Mazsa, 30-Aug-2021)

Ref Expression
Assertion dffunsALTV2 FunsALTV = f Rels | f I

Proof

Step Hyp Ref Expression
1 dffunsALTV FunsALTV = f Rels | f CnvRefRels
2 cosselcnvrefrels2 f CnvRefRels f I f Rels
3 cosselrels f Rels f Rels
4 3 biantrud f Rels f I f I f Rels
5 2 4 bitr4id f Rels f CnvRefRels f I
6 1 5 rabimbieq FunsALTV = f Rels | f I