Definition df-evpm

Description: Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018)

	Ref	Expression
Assertion	df-evpm	$$⊢\mathrm{pmEven}=\left(d\in \mathrm{V}⟼{\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cevpm	$$class\mathrm{pmEven}$$
1		vd	$$setvard$$
2		cvv	$$class\mathrm{V}$$
3		cpsgn	$$class\mathrm{pmSgn}$$
4	1	cv	$$setvard$$
5	4 3	cfv	$$class\mathrm{pmSgn}\left(d\right)$$
6	5	ccnv	$$class{\mathrm{pmSgn}\left(d\right)}^{-1}$$
7		c1	$$class1$$
8	7	csn	$$class\left\{1\right\}$$
9	6 8	cima	$$class{\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]$$
10	1 2 9	cmpt	$$class\left(d\in \mathrm{V}⟼{\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]\right)$$
11	0 10	wceq	$$wff\mathrm{pmEven}=\left(d\in \mathrm{V}⟼{\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]\right)$$