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 8

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmfsh	⊢ mFresh
1		c8	⊢ 8
2	1	cslot	⊢ Slot 8
3	0 2	wceq	⊢ mFresh = Slot 8