Metamath Proof Explorer

Theorem dffunsALTV

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

Ref Expression
Assertion dffunsALTV 
|- FunsALTV = { f e. Rels | ,~ f e. CnvRefRels }

Proof

Step Hyp Ref Expression
1 df-funsALTV 
 |-  FunsALTV = ( Funss i^i Rels )
2 df-funss 
 |-  Funss = { f | ,~ f e. CnvRefRels }
3 1 2 abeqin 
 |-  FunsALTV = { f e. Rels | ,~ f e. CnvRefRels }