Definition df-syms

Description: Define the class of all symmetric sets. It is used only by df-symrels .

Note the similarity of Definitions df-refs , df-syms and df-trs , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 19-Jul-2019)

	Ref	Expression
Assertion	df-syms	|- Syms = { x | `' ( x i^i ( dom x X. ran x ) ) _S ( x i^i ( dom x X. ran x ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csyms	|- Syms
1		vx	|- x
2	1	cv	|- x
3	2	cdm	|- dom x
4	2	crn	|- ran x
5	3 4	cxp	|- ( dom x X. ran x )
6	2 5	cin	|- ( x i^i ( dom x X. ran x ) )
7	6	ccnv	|- `' ( x i^i ( dom x X. ran x ) )
8		cssr	|- _S
9	7 6 8	wbr	|- `' ( x i^i ( dom x X. ran x ) ) _S ( x i^i ( dom x X. ran x ) )
10	9 1	cab	|- { x | `' ( x i^i ( dom x X. ran x ) ) _S ( x i^i ( dom x X. ran x ) ) }
11	0 10	wceq	|- Syms = { x | `' ( x i^i ( dom x X. ran x ) ) _S ( x i^i ( dom x X. ran x ) ) }