Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Metamath formal systems
df-mpps
Next ⟩
df-mthm
Metamath Proof Explorer
Ascii
Unicode
Definition
df-mpps
Description:
Define the set of provable pre-statements.
(Contributed by
Mario Carneiro
, 14-Jul-2016)
Ref
Expression
Assertion
df-mpps
⊢
mPPSt
=
t
∈
V
⟼
d
h
a
|
d
h
a
∈
mPreSt
⁡
t
∧
a
∈
d
mCls
⁡
t
h
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cmpps
class
mPPSt
1
vt
setvar
t
2
cvv
class
V
3
vd
setvar
d
4
vh
setvar
h
5
va
setvar
a
6
3
cv
setvar
d
7
4
cv
setvar
h
8
5
cv
setvar
a
9
6
7
8
cotp
class
d
h
a
10
cmpst
class
mPreSt
11
1
cv
setvar
t
12
11
10
cfv
class
mPreSt
⁡
t
13
9
12
wcel
wff
d
h
a
∈
mPreSt
⁡
t
14
cmcls
class
mCls
15
11
14
cfv
class
mCls
⁡
t
16
6
7
15
co
class
d
mCls
⁡
t
h
17
8
16
wcel
wff
a
∈
d
mCls
⁡
t
h
18
13
17
wa
wff
d
h
a
∈
mPreSt
⁡
t
∧
a
∈
d
mCls
⁡
t
h
19
18
3
4
5
coprab
class
d
h
a
|
d
h
a
∈
mPreSt
⁡
t
∧
a
∈
d
mCls
⁡
t
h
20
1
2
19
cmpt
class
t
∈
V
⟼
d
h
a
|
d
h
a
∈
mPreSt
⁡
t
∧
a
∈
d
mCls
⁡
t
h
21
0
20
wceq
wff
mPPSt
=
t
∈
V
⟼
d
h
a
|
d
h
a
∈
mPreSt
⁡
t
∧
a
∈
d
mCls
⁡
t
h