Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Metamath formal systems
df-mex
Metamath Proof Explorer
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 ‘ 𝑡 ) ) )