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

Definition df-evpm 16841
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 16839 . 2  class pmEven
2 vd . . 3  setvar  d
3 cvv 3059 . . 3  class  _V
42cv 1404 . . . . . 6  class  d
5 cpsgn 16838 . . . . . 6  class pmSgn
64, 5cfv 5569 . . . . 5  class  (pmSgn `  d )
76ccnv 4822 . . . 4  class  `' (pmSgn `  d )
8 c1 9523 . . . . 5  class  1
98csn 3972 . . . 4  class  { 1 }
107, 9cima 4826 . . 3  class  ( `' (pmSgn `  d ) " { 1 } )
112, 3, 10cmpt 4453 . 2  class  ( d  e.  _V  |->  ( `' (pmSgn `  d ) " { 1 } ) )
121, 11wceq 1405 1  wff pmEven  =  ( d  e.  _V  |->  ( `' (pmSgn `  d ) " { 1 } ) )
Colors of variables: wff setvar class
This definition is referenced by:  evpmss  18920  psgnevpmb  18921
  Copyright terms: Public domain W3C validator