Definition df-inr

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

	Ref	Expression
Assertion	df-inr	$$⊢inr=\left(x\in \mathrm{V}⟼⟨1_{𝑜},x⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinr	$$classinr$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		c1o	$$class{1}_{𝑜}$$
4	1	cv	$$setvarx$$
5	3 4	cop	$$class⟨1_{𝑜},x⟩$$
6	1 2 5	cmpt	$$class\left(x\in \mathrm{V}⟼⟨1_{𝑜},x⟩\right)$$
7	0 6	wceq	$$wffinr=\left(x\in \mathrm{V}⟼⟨1_{𝑜},x⟩\right)$$