MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-evpm Structured version   Unicode version

Definition df-evpm 16310
Description: Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.)
Assertion
Ref Expression
df-evpm  |- pmEven  =  ( d  e.  _V  |->  ( `' (pmSgn `  d ) " { 1 } ) )

Detailed syntax breakdown of Definition df-evpm
StepHypRef Expression
1 cevpm 16308 . 2  class pmEven
2 vd . . 3  setvar  d
3 cvv 3113 . . 3  class  _V
42cv 1378 . . . . . 6  class  d
5 cpsgn 16307 . . . . . 6  class pmSgn
64, 5cfv 5586 . . . . 5  class  (pmSgn `  d )
76ccnv 4998 . . . 4  class  `' (pmSgn `  d )
8 c1 9489 . . . . 5  class  1
98csn 4027 . . . 4  class  { 1 }
107, 9cima 5002 . . 3  class  ( `' (pmSgn `  d ) " { 1 } )
112, 3, 10cmpt 4505 . 2  class  ( d  e.  _V  |->  ( `' (pmSgn `  d ) " { 1 } ) )
121, 11wceq 1379 1  wff pmEven  =  ( d  e.  _V  |->  ( `' (pmSgn `  d ) " { 1 } ) )
Colors of variables: wff setvar class
This definition is referenced by:  evpmss  18386  psgnevpmb  18387
  Copyright terms: Public domain W3C validator