Metamath Proof Explorer

Definition df-mmax

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

Ref Expression
Assertion df-mmax 
|- mAx = Slot 5

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmax 
 |-  mAx
1 c5 
 |-  5
2 1 cslot 
 |-  Slot 5
3 0 2 wceq 
 |-  mAx = Slot 5