Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mex Structured version   Visualization version   GIF version

Definition df-mex 33162
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.)
Assertion
Ref Expression
df-mex mEx = (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))

Detailed syntax breakdown of Definition df-mex
StepHypRef Expression
1 cmex 33142 . 2 class mEx
2 vt . . 3 setvar 𝑡
3 cvv 3408 . . 3 class V
42cv 1542 . . . . 5 class 𝑡
5 cmtc 33139 . . . . 5 class mTC
64, 5cfv 6380 . . . 4 class (mTC‘𝑡)
7 cmrex 33141 . . . . 5 class mREx
84, 7cfv 6380 . . . 4 class (mREx‘𝑡)
96, 8cxp 5549 . . 3 class ((mTC‘𝑡) × (mREx‘𝑡))
102, 3, 9cmpt 5135 . 2 class (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))
111, 10wceq 1543 1 wff mEx = (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))
Colors of variables: wff setvar class
This definition is referenced by:  mexval  33177
  Copyright terms: Public domain W3C validator