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	$$⊢\mathrm{mDV}=\left(t\in \mathrm{V}⟼\left(\mathrm{mVR}\left(t\right)\times \mathrm{mVR}\left(t\right)\right)\setminus \mathrm{I}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmdv	$$class\mathrm{mDV}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		cmvar	$$class\mathrm{mVR}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class\mathrm{mVR}\left(t\right)$$
6	5 5	cxp	$$class\left(\mathrm{mVR}\left(t\right)\times \mathrm{mVR}\left(t\right)\right)$$
7		cid	$$class\mathrm{I}$$
8	6 7	cdif	$$class\left(\left(\mathrm{mVR}\left(t\right)\times \mathrm{mVR}\left(t\right)\right)\setminus \mathrm{I}\right)$$
9	1 2 8	cmpt	$$class\left(t\in \mathrm{V}⟼\left(\mathrm{mVR}\left(t\right)\times \mathrm{mVR}\left(t\right)\right)\setminus \mathrm{I}\right)$$
10	0 9	wceq	$$wff\mathrm{mDV}=\left(t\in \mathrm{V}⟼\left(\mathrm{mVR}\left(t\right)\times \mathrm{mVR}\left(t\right)\right)\setminus \mathrm{I}\right)$$