Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-exid Structured version   Visualization version   GIF version

Definition df-exid 35004
Description: A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
Assertion
Ref Expression
df-exid ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
Distinct variable group:   𝑥,𝑔,𝑦

Detailed syntax breakdown of Definition df-exid
StepHypRef Expression
1 cexid 35003 . 2 class ExId
2 vx . . . . . . . . 9 setvar 𝑥
32cv 1527 . . . . . . . 8 class 𝑥
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1527 . . . . . . . 8 class 𝑦
6 vg . . . . . . . . 9 setvar 𝑔
76cv 1527 . . . . . . . 8 class 𝑔
83, 5, 7co 7145 . . . . . . 7 class (𝑥𝑔𝑦)
98, 5wceq 1528 . . . . . 6 wff (𝑥𝑔𝑦) = 𝑦
105, 3, 7co 7145 . . . . . . 7 class (𝑦𝑔𝑥)
1110, 5wceq 1528 . . . . . 6 wff (𝑦𝑔𝑥) = 𝑦
129, 11wa 396 . . . . 5 wff ((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
137cdm 5548 . . . . . 6 class dom 𝑔
1413cdm 5548 . . . . 5 class dom dom 𝑔
1512, 4, 14wral 3135 . . . 4 wff 𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
1615, 2, 14wrex 3136 . . 3 wff 𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
1716, 6cab 2796 . 2 class {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
181, 17wceq 1528 1 wff ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  isexid  35006
  Copyright terms: Public domain W3C validator