Metamath Proof Explorer

Definition df-mfsh

Description: Define the freshness relation of a model. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mfsh 
|- mFresh = Slot ; 1 9

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfsh 
 |-  mFresh
1 c1 
 |-  1
2 c9 
 |-  9
3 1 2 cdc 
 |-  ; 1 9
4 3 cslot 
 |-  Slot ; 1 9
5 0 4 wceq 
 |-  mFresh = Slot ; 1 9