Definition df-syms

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

Note the similarity of the 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	$$⊢\mathrm{Syms}=\left\{x|{\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)}^{-1}\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csyms	$$class\mathrm{Syms}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3	2	cdm	$$class\mathrm{dom}x$$
4	2	crn	$$class\mathrm{ran}x$$
5	3 4	cxp	$$class\left(\mathrm{dom}x\times \mathrm{ran}x\right)$$
6	2 5	cin	$$class\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)$$
7	6	ccnv	$$class{\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)}^{-1}$$
8		cssr	$$class\mathrm{S}$$
9	7 6 8	wbr	$$wff{\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)}^{-1}\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)$$
10	9 1	cab	$$class\left\{x|{\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)}^{-1}\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\right\}$$
11	0 10	wceq	$$wff\mathrm{Syms}=\left\{x|{\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)}^{-1}\mathrm{S}\left(x\cap \left(\mathrm{dom}x\times \mathrm{ran}x\right)\right)\right\}$$