MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-exid Unicode version

Definition df-exid 20998
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  =  { g  |  E. x  e.  dom  dom  g A. y  e.  dom  dom  g ( ( x g y )  =  y  /\  ( y g x )  =  y ) }
Distinct variable group:    x, g, y

Detailed syntax breakdown of Definition df-exid
StepHypRef Expression
1 cexid 20997 . 2  class  ExId
2 vx . . . . . . . . 9  set  x
32cv 1631 . . . . . . . 8  class  x
4 vy . . . . . . . . 9  set  y
54cv 1631 . . . . . . . 8  class  y
6 vg . . . . . . . . 9  set  g
76cv 1631 . . . . . . . 8  class  g
83, 5, 7co 5874 . . . . . . 7  class  ( x g y )
98, 5wceq 1632 . . . . . 6  wff  ( x g y )  =  y
105, 3, 7co 5874 . . . . . . 7  class  ( y g x )
1110, 5wceq 1632 . . . . . 6  wff  ( y g x )  =  y
129, 11wa 358 . . . . 5  wff  ( ( x g y )  =  y  /\  (
y g x )  =  y )
137cdm 4705 . . . . . 6  class  dom  g
1413cdm 4705 . . . . 5  class  dom  dom  g
1512, 4, 14wral 2556 . . . 4  wff  A. y  e.  dom  dom  g (
( x g y )  =  y  /\  ( y g x )  =  y )
1615, 2, 14wrex 2557 . . 3  wff  E. x  e.  dom  dom  g A. y  e.  dom  dom  g
( ( x g y )  =  y  /\  ( y g x )  =  y )
1716, 6cab 2282 . 2  class  { g  |  E. x  e. 
dom  dom  g A. y  e.  dom  dom  g (
( x g y )  =  y  /\  ( y g x )  =  y ) }
181, 17wceq 1632 1  wff  ExId  =  { g  |  E. x  e.  dom  dom  g A. y  e.  dom  dom  g ( ( x g y )  =  y  /\  ( y g x )  =  y ) }
Colors of variables: wff set class
This definition is referenced by:  isexid  21000
  Copyright terms: Public domain W3C validator