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 e. _V |-> ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmthm 
 |-  mThm
1 vt 
 |-  t
2 cvv 
 |-  _V
3 cmsr 
 |-  mStRed
4 1 cv 
 |-  t
5 4 3 cfv 
 |-  ( mStRed ` t )
6 5 ccnv 
 |-  `' ( mStRed ` t )
7 cmpps 
 |-  mPPSt
8 4 7 cfv 
 |-  ( mPPSt ` t )
9 5 8 cima 
 |-  ( ( mStRed ` t ) " ( mPPSt ` t ) )
10 6 9 cima 
 |-  ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) )
11 1 2 10 cmpt 
 |-  ( t e. _V |-> ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) ) )
12 0 11 wceq 
 |-  mThm = ( t e. _V |-> ( `' ( mStRed ` t ) " ( ( mStRed ` t ) " ( mPPSt ` t ) ) ) )