Metamath Proof Explorer


Theorem dfhe2

Description: The property of relation R being hereditary in class A . (Contributed by RP, 27-Mar-2020)

Ref Expression
Assertion dfhe2 R hereditary A R A A × A

Proof

Step Hyp Ref Expression
1 df-he R hereditary A R A A
2 resssxp R A A R A A × A
3 1 2 bitri R hereditary A R A A × A