Metamath Proof Explorer


Definition df-mex

Description: Define the set of expressions, which are strings of constants and variables headed by a typecode constant. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mex mEx = ( 𝑡 ∈ V ↦ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmex mEx
1 vt 𝑡
2 cvv V
3 cmtc mTC
4 1 cv 𝑡
5 4 3 cfv ( mTC ‘ 𝑡 )
6 cmrex mREx
7 4 6 cfv ( mREx ‘ 𝑡 )
8 5 7 cxp ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) )
9 1 2 8 cmpt ( 𝑡 ∈ V ↦ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) )
10 0 9 wceq mEx = ( 𝑡 ∈ V ↦ ( ( mTC ‘ 𝑡 ) × ( mREx ‘ 𝑡 ) ) )