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 33273
 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 33272 . 2 class ExId
2 vx . . . . . . . . 9 setvar 𝑥
32cv 1479 . . . . . . . 8 class 𝑥
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1479 . . . . . . . 8 class 𝑦
6 vg . . . . . . . . 9 setvar 𝑔
76cv 1479 . . . . . . . 8 class 𝑔
83, 5, 7co 6604 . . . . . . 7 class (𝑥𝑔𝑦)
98, 5wceq 1480 . . . . . 6 wff (𝑥𝑔𝑦) = 𝑦
105, 3, 7co 6604 . . . . . . 7 class (𝑦𝑔𝑥)
1110, 5wceq 1480 . . . . . 6 wff (𝑦𝑔𝑥) = 𝑦
129, 11wa 384 . . . . 5 wff ((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
137cdm 5074 . . . . . 6 class dom 𝑔
1413cdm 5074 . . . . 5 class dom dom 𝑔
1512, 4, 14wral 2907 . . . 4 wff 𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
1615, 2, 14wrex 2908 . . 3 wff 𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)
1716, 6cab 2607 . 2 class {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
181, 17wceq 1480 1 wff ExId = {𝑔 ∣ ∃𝑥 ∈ dom dom 𝑔𝑦 ∈ dom dom 𝑔((𝑥𝑔𝑦) = 𝑦 ∧ (𝑦𝑔𝑥) = 𝑦)}
 Colors of variables: wff setvar class This definition is referenced by:  isexid  33275
 Copyright terms: Public domain W3C validator