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

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

Detailed syntax breakdown of Definition df-ref
StepHypRef Expression
1 cref 20515 . 2  class  Ref
2 vy . . . . . . 7  setvar  y
32cv 1436 . . . . . 6  class  y
43cuni 4219 . . . . 5  class  U. y
5 vx . . . . . . 7  setvar  x
65cv 1436 . . . . . 6  class  x
76cuni 4219 . . . . 5  class  U. x
84, 7wceq 1437 . . . 4  wff  U. y  =  U. x
9 vz . . . . . . . 8  setvar  z
109cv 1436 . . . . . . 7  class  z
11 vw . . . . . . . 8  setvar  w
1211cv 1436 . . . . . . 7  class  w
1310, 12wss 3436 . . . . . 6  wff  z  C_  w
1413, 11, 3wrex 2772 . . . . 5  wff  E. w  e.  y  z  C_  w
1514, 9, 6wral 2771 . . . 4  wff  A. z  e.  x  E. w  e.  y  z  C_  w
168, 15wa 370 . . 3  wff  ( U. y  =  U. x  /\  A. z  e.  x  E. w  e.  y 
z  C_  w )
1716, 5, 2copab 4481 . 2  class  { <. x ,  y >.  |  ( U. y  =  U. x  /\  A. z  e.  x  E. w  e.  y  z  C_  w
) }
181, 17wceq 1437 1  wff  Ref  =  { <. x ,  y
>.  |  ( U. y  =  U. x  /\  A. z  e.  x  E. w  e.  y 
z  C_  w ) }
Colors of variables: wff setvar class
This definition is referenced by:  refrel  20521  isref  20522
  Copyright terms: Public domain W3C validator