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 | x = y z x z y 𝒫 z
2 1 relopabiv Rel Fne