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

Definition df-ref 26335
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 26331 . 2  class  Ref
2 vx . . . . . . 7  set  x
32cv 1651 . . . . . 6  class  x
43cuni 4007 . . . . 5  class  U. x
5 vy . . . . . . 7  set  y
65cv 1651 . . . . . 6  class  y
76cuni 4007 . . . . 5  class  U. y
84, 7wceq 1652 . . . 4  wff  U. x  =  U. y
9 vz . . . . . . . 8  set  z
109cv 1651 . . . . . . 7  class  z
11 vw . . . . . . . 8  set  w
1211cv 1651 . . . . . . 7  class  w
1310, 12wss 3312 . . . . . 6  wff  z  C_  w
1413, 11, 3wrex 2698 . . . . 5  wff  E. w  e.  x  z  C_  w
1514, 9, 6wral 2697 . . . 4  wff  A. z  e.  y  E. w  e.  x  z  C_  w
168, 15wa 359 . . 3  wff  ( U. x  =  U. y  /\  A. z  e.  y  E. w  e.  x  z  C_  w )
1716, 2, 5copab 4257 . 2  class  { <. x ,  y >.  |  ( U. x  =  U. y  /\  A. z  e.  y  E. w  e.  x  z  C_  w
) }
181, 17wceq 1652 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  26349  isref  26350
  Copyright terms: Public domain W3C validator