Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mdv Structured version   Visualization version   Unicode version
Definition df-mdv 31385
Description: Define the set of distinct variable conditions, which are pairs of distinct variables. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mdv |- mDV = ( t e. _V |-> ( ( (mVR ` t ) X. (mVR ` t ) ) \ _I ) )
Detailed syntax breakdown of Definition df-mdv
StepHypRef Expression
1 cmdv 31365 . 2 class mDV
2 vt . . 3 setvar t
3 cvv 3200 . . 3 class _V
42cv 1482 . . . . . 6 class t
5 cmvar 31358 . . . . . 6 class mVR
64, 5cfv 5888 . . . . 5 class (mVR ` t )
76, 6cxp 5112 . . . 4 class ( (mVR ` t ) X. (mVR ` t ) )
8 cid 5023 . . . 4 class _I
97, 8cdif 3571 . . 3 class ( ( (mVR ` t ) X. (mVR ` t ) ) \ _I )
102, 3, 9cmpt 4729 . 2 class ( t e. _V |-> ( ( (mVR ` t ) X. (mVR ` t ) ) \ _I ) )
111, 10wceq 1483 1 wff mDV = ( t e. _V |-> ( ( (mVR ` t ) X. (mVR ` t ) ) \ _I ) )
Colors of variables: wff setvar class
This definition is referenced by:  mdvval  31401
  Copyright terms: Public domain W3C validator