df-syms

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

		Ref	Expression
	Assertion	df-syms	$⊢ Syms = \{x \| {(x \cap (dom x \times ran x))}^{-1} S (x \cap (dom x \times ran x))\}$

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

Metamath Proof Explorer