Metamath Proof Explorer

Definition df-funsALTV

Description: Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV , ... , dffunsALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021)

Ref Expression
Assertion df-funsALTV 
|- FunsALTV = ( Funss i^i Rels )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfunsALTV 
 |-  FunsALTV
1 cfunss 
 |-  Funss
2 crels 
 |-  Rels
3 1 2 cin 
 |-  ( Funss i^i Rels )
4 0 3 wceq 
 |-  FunsALTV = ( Funss i^i Rels )