Definition df-he 38067

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

Assertion

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

Detailed syntax breakdown of Definition df-he

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	whe 38066	. 2 wff R hereditary A
4	2, 1	cima 5117	. . 3 class ( R " A )
5	4, 1	wss 3574	. 2 wff ( R " A ) C_ A
6	3, 5	wb 196	1 wff ( R hereditary A <-> ( R " A ) C_ A )

This definition is referenced by:  dfhe2  38068  dfhe3  38069  heeq12  38070  sbcheg  38073  hess  38074  xphe  38075  0he  38076  he0  38078  unhe1  38079  snhesn  38080  dffrege76  38233