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 = { 𝑔 ∣ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cexid	⊢ ExId
1		vg	⊢ 𝑔
2		vx	⊢ 𝑥
3	1	cv	⊢ 𝑔
4	3	cdm	⊢ dom 𝑔
5	4	cdm	⊢ dom dom 𝑔
6		vy	⊢ 𝑦
7	2	cv	⊢ 𝑥
8	6	cv	⊢ 𝑦
9	7 8 3	co	⊢ ( 𝑥 𝑔 𝑦 )
10	9 8	wceq	⊢ ( 𝑥 𝑔 𝑦 ) = 𝑦
11	8 7 3	co	⊢ ( 𝑦 𝑔 𝑥 )
12	11 8	wceq	⊢ ( 𝑦 𝑔 𝑥 ) = 𝑦
13	10 12	wa	⊢ ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 )
14	13 6 5	wral	⊢ ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 )
15	14 2 5	wrex	⊢ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 )
16	15 1	cab	⊢ { 𝑔 ∣ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) }
17	0 16	wceq	⊢ ExId = { 𝑔 ∣ ∃ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) = 𝑦 ∧ ( 𝑦 𝑔 𝑥 ) = 𝑦 ) }