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	$$⊢\mathrm{FunsALTV}=\mathrm{Funss}\cap \mathrm{Rels}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfunsALTV	$$class\mathrm{FunsALTV}$$
1		cfunss	$$class\mathrm{Funss}$$
2		crels	$$class\mathrm{Rels}$$
3	1 2	cin	$$class\left(\mathrm{Funss}\cap \mathrm{Rels}\right)$$
4	0 3	wceq	$$wff\mathrm{FunsALTV}=\mathrm{Funss}\cap \mathrm{Rels}$$