Definition df-funss

Description: Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV ). It is used only by df-funsALTV . (Contributed by Peter Mazsa, 17-Jul-2021)

	Ref	Expression
Assertion	df-funss	$$⊢\mathrm{Funss}=\left\{x|\wr x\in \mathrm{CnvRefRels}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfunss	$$class\mathrm{Funss}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3	2	ccoss	$$class\wr x$$
4		ccnvrefrels	$$class\mathrm{CnvRefRels}$$
5	3 4	wcel	$$wff\wr x\in \mathrm{CnvRefRels}$$
6	5 1	cab	$$class\left\{x|\wr x\in \mathrm{CnvRefRels}\right\}$$
7	0 6	wceq	$$wff\mathrm{Funss}=\left\{x|\wr x\in \mathrm{CnvRefRels}\right\}$$