Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Models of formal systems
df-mfsh
Next ⟩
df-mevl
Metamath Proof Explorer
Ascii
Unicode
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
class
mFresh
1
c8
class
8
2
1
cslot
class
Slot
8
3
0
2
wceq
wff
mFresh
=
Slot
8