Metamath Proof Explorer

Theorem 0he

Description: The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020)

Ref Expression
Assertion 0he 
|- (/) hereditary A

Proof

Step Hyp Ref Expression
1 0ima 
 |-  ( (/) " A ) = (/)
2 0ss 
 |-  (/) C_ A
3 1 2 eqsstri 
 |-  ( (/) " A ) C_ A
4 df-he 
 |-  ( (/) hereditary A <-> ( (/) " A ) C_ A )
5 3 4 mpbir 
 |-  (/) hereditary A