Metamath Proof Explorer

Theorem fnerel

Description: Fineness is a relation. (Contributed by Jeff Hankins, 28-Sep-2009)

Ref Expression
Assertion fnerel 
|- Rel Fne

Proof

Step Hyp Ref Expression
1 df-fne 
 |-  Fne = { <. x , y >. | ( U. x = U. y /\ A. z e. x z C_ U. ( y i^i ~P z ) ) }
2 1 relopabiv 
 |-  Rel Fne