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 A × A
2 dfhe2 I hereditary A I A A × A
3 1 2 mpbir I hereditary A