This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-inr

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

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

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