Metamath Proof Explorer

Definition df-mcn

Description: Define the set of constants in a Metamath formal system. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mcn 
|- mCN = Slot 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmcn 
 |-  mCN
1 c1 
 |-  1
2 1 cslot 
 |-  Slot 1
3 0 2 wceq 
 |-  mCN = Slot 1