Definition df-inr

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

	Ref	Expression
Assertion	df-inr	|- inr = ( x e. _V |-> <. 1o , x >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinr	|- inr
1		vx	|- x
2		cvv	|- _V
3		c1o	|- 1o
4	1	cv	|- x
5	3 4	cop	|- <. 1o , x >.
6	1 2 5	cmpt	|- ( x e. _V |-> <. 1o , x >. )
7	0 6	wceq	|- inr = ( x e. _V |-> <. 1o , x >. )