Definition df-inl

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

	Ref	Expression
Assertion	df-inl	$$⊢inl=\left(x\in \mathrm{V}⟼⟨\varnothing ,x⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinl	$$classinl$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		c0	$$class\varnothing$$
4	1	cv	$$setvarx$$
5	3 4	cop	$$class⟨\varnothing ,x⟩$$
6	1 2 5	cmpt	$$class\left(x\in \mathrm{V}⟼⟨\varnothing ,x⟩\right)$$
7	0 6	wceq	$$wffinl=\left(x\in \mathrm{V}⟼⟨\varnothing ,x⟩\right)$$