Definition df-inl

Description: Left injection of a disjoint union. (Contributed by Mario Carneiro, 21-Jun-2022)

	Ref	Expression
Assertion	df-inl	|- inl = ( x e. _V |-> <. (/) , x >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinl	|- inl
1		vx	|- x
2		cvv	|- _V
3		c0	|- (/)
4	1	cv	|- x
5	3 4	cop	|- <. (/) , x >.
6	1 2 5	cmpt	|- ( x e. _V |-> <. (/) , x >. )
7	0 6	wceq	|- inl = ( x e. _V |-> <. (/) , x >. )