Metamath Proof Explorer

Definition df-exid

Description: A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-exid	$⊢ ExId = \{g \| \exists x \in dom dom g \forall y \in dom dom g (x g y = y \land y g x = y)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cexid	$class ExId$
1		vg	$setvar g$
2		vx	$setvar x$
3	1	cv	$setvar g$
4	3	cdm	$class dom g$
5	4	cdm	$class dom dom g$
6		vy	$setvar y$
7	2	cv	$setvar x$
8	6	cv	$setvar y$
9	7 8 3	co	$class (x g y)$
10	9 8	wceq	$wff x g y = y$
11	8 7 3	co	$class (y g x)$
12	11 8	wceq	$wff y g x = y$
13	10 12	wa	$wff (x g y = y \land y g x = y)$
14	13 6 5	wral	$wff \forall y \in dom dom g (x g y = y \land y g x = y)$
15	14 2 5	wrex	$wff \exists x \in dom dom g \forall y \in dom dom g (x g y = y \land y g x = y)$
16	15 1	cab	$class \{g \| \exists x \in dom dom g \forall y \in dom dom g (x g y = y \land y g x = y)\}$
17	0 16	wceq	$wff ExId = \{g \| \exists x \in dom dom g \forall y \in dom dom g (x g y = y \land y g x = y)\}$