Metamath Proof Explorer

Theorem he0

Description: Any relation is hereditary in the empty set. (Contributed by RP, 27-Mar-2020)

Ref Expression
Assertion he0 
|- A hereditary (/)

Proof

Step Hyp Ref Expression
1 ima0 
 |-  ( A " (/) ) = (/)
2 1 eqimssi 
 |-  ( A " (/) ) C_ (/)
3 df-he 
 |-  ( A hereditary (/) <-> ( A " (/) ) C_ (/) )
4 2 3 mpbir 
 |-  A hereditary (/)