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 31722
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 31702 . 2 class mEx
2 vt . . 3 setvar 𝑡
3 cvv 3351 . . 3 class V
42cv 1630 . . . . 5 class 𝑡
5 cmtc 31699 . . . . 5 class mTC
64, 5cfv 6030 . . . 4 class (mTC‘𝑡)
7 cmrex 31701 . . . . 5 class mREx
84, 7cfv 6030 . . . 4 class (mREx‘𝑡)
96, 8cxp 5248 . . 3 class ((mTC‘𝑡) × (mREx‘𝑡))
102, 3, 9cmpt 4864 . 2 class (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))
111, 10wceq 1631 1 wff mEx = (𝑡 ∈ V ↦ ((mTC‘𝑡) × (mREx‘𝑡)))
Colors of variables: wff setvar class
This definition is referenced by:  mexval  31737
  Copyright terms: Public domain W3C validator