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	⊢ Syms = { 𝑥 ∣ ◡ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csyms	⊢ Syms
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2	cdm	⊢ dom 𝑥
4	2	crn	⊢ ran 𝑥
5	3 4	cxp	⊢ ( dom 𝑥 × ran 𝑥 )
6	2 5	cin	⊢ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
7	6	ccnv	⊢ ◡ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
8		cssr	⊢ S
9	7 6 8	wbr	⊢ ◡ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
10	9 1	cab	⊢ { 𝑥 ∣ ◡ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }
11	0 10	wceq	⊢ Syms = { 𝑥 ∣ ◡ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }