Metamath Proof Explorer

Theorem idhe

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

Ref Expression
Assertion idhe 
|- _I hereditary A

Proof

Step Hyp Ref Expression
1 idssxp 
 |-  ( _I |` A ) C_ ( A X. A )
2 dfhe2 
 |-  ( _I hereditary A <-> ( _I |` A ) C_ ( A X. A ) )
3 1 2 mpbir 
 |-  _I hereditary A