Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mpps Structured version   Unicode version

Definition df-mpps 30144
 Description: Define the set of provable pre-statements. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mpps mPPSt mPreSt mCls
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-mpps
StepHypRef Expression
1 cmpps 30124 . 2 mPPSt
2 vt . . 3
3 cvv 3080 . . 3
4 vd . . . . . . . 8
54cv 1436 . . . . . . 7
6 vh . . . . . . . 8
76cv 1436 . . . . . . 7
8 va . . . . . . . 8
98cv 1436 . . . . . . 7
105, 7, 9cotp 4006 . . . . . 6
112cv 1436 . . . . . . 7
12 cmpst 30119 . . . . . . 7 mPreSt
1311, 12cfv 5601 . . . . . 6 mPreSt
1410, 13wcel 1872 . . . . 5 mPreSt
15 cmcls 30123 . . . . . . . 8 mCls
1611, 15cfv 5601 . . . . . . 7 mCls
175, 7, 16co 6305 . . . . . 6 mCls
189, 17wcel 1872 . . . . 5 mCls
1914, 18wa 370 . . . 4 mPreSt mCls
2019, 4, 6, 8coprab 6306 . . 3 mPreSt mCls
212, 3, 20cmpt 4482 . 2 mPreSt mCls
221, 21wceq 1437 1 mPPSt mPreSt mCls
 Colors of variables: wff setvar class This definition is referenced by:  mppsval  30218
 Copyright terms: Public domain W3C validator