Definition df-msax 31498

Description: Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-msax	|- mSAX = ( t e. _V |-> ( p e. (mSA ` t ) |-> ( (mVH ` t ) " ( (mVars ` t ) ` p ) ) ) )

Distinct variable group:   t, p

Detailed syntax breakdown of Definition df-msax

Step	Hyp	Ref	Expression
1		cmsax 31490	. 2 class mSAX
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vp	. . . 4 setvar p
5	2	cv 1482	. . . . 5 class t
6		cmsa 31483	. . . . 5 class mSA
7	5, 6	cfv 5888	. . . 4 class (mSA ` t )
8		cmvh 31369	. . . . . 6 class mVH
9	5, 8	cfv 5888	. . . . 5 class (mVH ` t )
10	4	cv 1482	. . . . . 6 class p
11		cmvrs 31366	. . . . . . 7 class mVars
12	5, 11	cfv 5888	. . . . . 6 class (mVars ` t )
13	10, 12	cfv 5888	. . . . 5 class ( (mVars ` t ) ` p )
14	9, 13	cima 5117	. . . 4 class ( (mVH ` t ) " ( (mVars ` t ) ` p ) )
15	4, 7, 14	cmpt 4729	. . 3 class ( p e. (mSA ` t ) |-> ( (mVH ` t ) " ( (mVars ` t ) ` p ) ) )
16	2, 3, 15	cmpt 4729	. 2 class ( t e. _V |-> ( p e. (mSA ` t ) |-> ( (mVH ` t ) " ( (mVars ` t ) ` p ) ) ) )
17	1, 16	wceq 1483	1 wff mSAX = ( t e. _V |-> ( p e. (mSA ` t ) |-> ( (mVH ` t ) " ( (mVars ` t ) ` p ) ) ) )

This definition is referenced by: (None)