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 ) C_ ( A X. A ) )

Proof

Step Hyp Ref Expression
1 df-he 
 |-  ( R hereditary A <-> ( R " A ) C_ A )
2 resssxp 
 |-  ( ( R " A ) C_ A <-> ( R |` A ) C_ ( A X. A ) )
3 1 2 bitri 
 |-  ( R hereditary A <-> ( R |` A ) C_ ( A X. A ) )