Metamath Proof Explorer


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