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

Definition df-evpm 16120
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 16118 . 2  class pmEven
2 vd . . 3  setvar  d
3 cvv 3078 . . 3  class  _V
42cv 1369 . . . . . 6  class  d
5 cpsgn 16117 . . . . . 6  class pmSgn
64, 5cfv 5529 . . . . 5  class  (pmSgn `  d )
76ccnv 4950 . . . 4  class  `' (pmSgn `  d )
8 c1 9397 . . . . 5  class  1
98csn 3988 . . . 4  class  { 1 }
107, 9cima 4954 . . 3  class  ( `' (pmSgn `  d ) " { 1 } )
112, 3, 10cmpt 4461 . 2  class  ( d  e.  _V  |->  ( `' (pmSgn `  d ) " { 1 } ) )
121, 11wceq 1370 1  wff pmEven  =  ( d  e.  _V  |->  ( `' (pmSgn `  d ) " { 1 } ) )
Colors of variables: wff setvar class
This definition is referenced by:  evpmss  18144  psgnevpmb  18145
  Copyright terms: Public domain W3C validator