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 = (/) ) )