Metamath Proof Explorer

Theorem refrel

Description: Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

Ref Expression
Assertion refrel 
|- Rel Ref

Proof

Step Hyp Ref Expression
1 df-ref 
 |-  Ref = { <. x , y >. | ( U. y = U. x /\ A. z e. x E. w e. y z C_ w ) }
2 1 relopabiv 
 |-  Rel Ref