Metamath Proof Explorer


Theorem relen

Description: Equinumerosity is a relation. (Contributed by NM, 28-Mar-1998)

Ref Expression
Assertion relen Rel

Proof

Step Hyp Ref Expression
1 df-en = x y | f f : x 1-1 onto y
2 1 relopabiv Rel