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