Definition df-singleton

Description: Define the singleton function. See brsingle for its value. (Contributed by Scott Fenton, 4-Apr-2014)

	Ref	Expression
Assertion	df-singleton	⊢ Singleton = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csingle	⊢ Singleton
1		cvv	⊢ V
2	1 1	cxp	⊢ ( V × V )
3		cep	⊢ E
4	1 3	ctxp	⊢ ( V ⊗ E )
5		cid	⊢ I
6	5 1	ctxp	⊢ ( I ⊗ V )
7	4 6	csymdif	⊢ ( ( V ⊗ E ) △ ( I ⊗ V ) )
8	7	crn	⊢ ran ( ( V ⊗ E ) △ ( I ⊗ V ) )
9	2 8	cdif	⊢ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) )
10	0 9	wceq	⊢ Singleton = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) )