Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Metamath formal systems
df-mthm
Next ⟩
mvtval
Metamath Proof Explorer
Ascii
Unicode
Definition
df-mthm
Description:
Define the set of theorems.
(Contributed by
Mario Carneiro
, 14-Jul-2016)
Ref
Expression
Assertion
df-mthm
⊢
mThm
=
t
∈
V
⟼
mStRed
⁡
t
-1
mStRed
⁡
t
mPPSt
⁡
t
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cmthm
class
mThm
1
vt
setvar
t
2
cvv
class
V
3
cmsr
class
mStRed
4
1
cv
setvar
t
5
4
3
cfv
class
mStRed
⁡
t
6
5
ccnv
class
mStRed
⁡
t
-1
7
cmpps
class
mPPSt
8
4
7
cfv
class
mPPSt
⁡
t
9
5
8
cima
class
mStRed
⁡
t
mPPSt
⁡
t
10
6
9
cima
class
mStRed
⁡
t
-1
mStRed
⁡
t
mPPSt
⁡
t
11
1
2
10
cmpt
class
t
∈
V
⟼
mStRed
⁡
t
-1
mStRed
⁡
t
mPPSt
⁡
t
12
0
11
wceq
wff
mThm
=
t
∈
V
⟼
mStRed
⁡
t
-1
mStRed
⁡
t
mPPSt
⁡
t