Metamath Proof Explorer

Definition df-msax

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

Ref Expression
Assertion df-msax ⊢ mSAX = t ∈ V ⟼ p ∈ mSA ⁡ t ⟼ mVH ⁡ t mVars ⁡ t ⁡ p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmsax class mSAX
1 vt setvar t
2 cvv class V
3 vp setvar p
4 cmsa class mSA
5 1 cv setvar t
6 5 4 cfv class mSA ⁡ t
7 cmvh class mVH
8 5 7 cfv class mVH ⁡ t
9 cmvrs class mVars
10 5 9 cfv class mVars ⁡ t
11 3 cv setvar p
12 11 10 cfv class mVars ⁡ t ⁡ p
13 8 12 cima class mVH ⁡ t mVars ⁡ t ⁡ p
14 3 6 13 cmpt class p ∈ mSA ⁡ t ⟼ mVH ⁡ t mVars ⁡ t ⁡ p
15 1 2 14 cmpt class t ∈ V ⟼ p ∈ mSA ⁡ t ⟼ mVH ⁡ t mVars ⁡ t ⁡ p
16 0 15 wceq wff mSAX = t ∈ V ⟼ p ∈ mSA ⁡ t ⟼ mVH ⁡ t mVars ⁡ t ⁡ p