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 = ( 𝑡 ∈ V ↦ ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmdv	⊢ mDV
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		cmvar	⊢ mVR
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mVR ‘ 𝑡 )
6	5 5	cxp	⊢ ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) )
7		cid	⊢ I
8	6 7	cdif	⊢ ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I )
9	1 2 8	cmpt	⊢ ( 𝑡 ∈ V ↦ ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I ) )
10	0 9	wceq	⊢ mDV = ( 𝑡 ∈ V ↦ ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I ) )