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	|- Funss = { x | ,~ x e. CnvRefRels }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfunss	|- Funss
1		vx	|- x
2	1	cv	|- x
3	2	ccoss	|- ,~ x
4		ccnvrefrels	|- CnvRefRels
5	3 4	wcel	|- ,~ x e. CnvRefRels
6	5 1	cab	|- { x | ,~ x e. CnvRefRels }
7	0 6	wceq	|- Funss = { x | ,~ x e. CnvRefRels }