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 | ∃ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g x g y = y ∧ 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 ∧ y g x = y
14 13 6 5 wral wff ∀ y ∈ dom ⁡ dom ⁡ g x g y = y ∧ y g x = y
15 14 2 5 wrex wff ∃ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g x g y = y ∧ y g x = y
16 15 1 cab class g | ∃ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g x g y = y ∧ y g x = y
17 0 16 wceq wff ExId = g | ∃ x ∈ dom ⁡ dom ⁡ g ∀ y ∈ dom ⁡ dom ⁡ g x g y = y ∧ y g x = y