Metamath Proof Explorer

Definition df-mdv

Description: Define the set of distinct variable conditions, which are pairs of distinct variables. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mdv 
|- mDV = ( t e. _V |-> ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmdv 
 |-  mDV
1 vt 
 |-  t
2 cvv 
 |-  _V
3 cmvar 
 |-  mVR
4 1 cv 
 |-  t
5 4 3 cfv 
 |-  ( mVR ` t )
6 5 5 cxp 
 |-  ( ( mVR ` t ) X. ( mVR ` t ) )
7 cid 
 |-  _I
8 6 7 cdif 
 |-  ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I )
9 1 2 8 cmpt 
 |-  ( t e. _V |-> ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I ) )
10 0 9 wceq 
 |-  mDV = ( t e. _V |-> ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I ) )