Metamath Proof Explorer


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 = { 𝑥 ( 𝑥 ∩ ( 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 𝑥 ) ) }