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

Definition df-exid 21903
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 21902 . 2  class  ExId
2 vx . . . . . . . . 9  set  x
32cv 1651 . . . . . . . 8  class  x
4 vy . . . . . . . . 9  set  y
54cv 1651 . . . . . . . 8  class  y
6 vg . . . . . . . . 9  set  g
76cv 1651 . . . . . . . 8  class  g
83, 5, 7co 6081 . . . . . . 7  class  ( x g y )
98, 5wceq 1652 . . . . . 6  wff  ( x g y )  =  y
105, 3, 7co 6081 . . . . . . 7  class  ( y g x )
1110, 5wceq 1652 . . . . . 6  wff  ( y g x )  =  y
129, 11wa 359 . . . . 5  wff  ( ( x g y )  =  y  /\  (
y g x )  =  y )
137cdm 4878 . . . . . 6  class  dom  g
1413cdm 4878 . . . . 5  class  dom  dom  g
1512, 4, 14wral 2705 . . . 4  wff  A. y  e.  dom  dom  g (
( x g y )  =  y  /\  ( y g x )  =  y )
1615, 2, 14wrex 2706 . . 3  wff  E. x  e.  dom  dom  g A. y  e.  dom  dom  g
( ( x g y )  =  y  /\  ( y g x )  =  y )
1716, 6cab 2422 . 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 1652 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  21905
  Copyright terms: Public domain W3C validator