Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ref Unicode version

Definition df-ref 26367
Description: Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.)
Assertion
Ref Expression
df-ref  |-  Ref  =  { <. x ,  y
>.  |  ( U. x  =  U. y  /\  A. z  e.  y  E. w  e.  x  z  C_  w ) }
Distinct variable group:    x, w, y, z

Detailed syntax breakdown of Definition df-ref
StepHypRef Expression
1 cref 26363 . 2  class  Ref
2 vx . . . . . . 7  set  x
32cv 1631 . . . . . 6  class  x
43cuni 3843 . . . . 5  class  U. x
5 vy . . . . . . 7  set  y
65cv 1631 . . . . . 6  class  y
76cuni 3843 . . . . 5  class  U. y
84, 7wceq 1632 . . . 4  wff  U. x  =  U. y
9 vz . . . . . . . 8  set  z
109cv 1631 . . . . . . 7  class  z
11 vw . . . . . . . 8  set  w
1211cv 1631 . . . . . . 7  class  w
1310, 12wss 3165 . . . . . 6  wff  z  C_  w
1413, 11, 3wrex 2557 . . . . 5  wff  E. w  e.  x  z  C_  w
1514, 9, 6wral 2556 . . . 4  wff  A. z  e.  y  E. w  e.  x  z  C_  w
168, 15wa 358 . . 3  wff  ( U. x  =  U. y  /\  A. z  e.  y  E. w  e.  x  z  C_  w )
1716, 2, 5copab 4092 . 2  class  { <. x ,  y >.  |  ( U. x  =  U. y  /\  A. z  e.  y  E. w  e.  x  z  C_  w
) }
181, 17wceq 1632 1  wff  Ref  =  { <. x ,  y
>.  |  ( U. x  =  U. y  /\  A. z  e.  y  E. w  e.  x  z  C_  w ) }
Colors of variables: wff set class
This definition is referenced by:  refrel  26381  isref  26382
  Copyright terms: Public domain W3C validator