Metamath Proof Explorer


Theorem relrn0

Description: A relation is empty iff its range is empty. (Contributed by NM, 15-Sep-2004)

Ref Expression
Assertion relrn0 Rel A A = ran A =

Proof

Step Hyp Ref Expression
1 reldm0 Rel A A = dom A =
2 dm0rn0 dom A = ran A =
3 1 2 bitrdi Rel A A = ran A =