Metamath Proof Explorer

Definition df-he

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

Ref Expression
Assertion df-he 
|- ( R hereditary A <-> ( R " A ) C_ A )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 cA 
 |-  A
2 1 0 whe 
 |-  R hereditary A
3 0 1 cima 
 |-  ( R " A )
4 3 1 wss 
 |-  ( R " A ) C_ A
5 2 4 wb 
 |-  ( R hereditary A <-> ( R " A ) C_ A )