Definition df-he 41349

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

Assertion

Ref	Expression
df-he	⊢ (𝑅 hereditary 𝐴 ↔ (𝑅 “ 𝐴) ⊆ 𝐴)

Detailed syntax breakdown of Definition df-he

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	whe 41348	. 2 wff 𝑅 hereditary 𝐴
4	2, 1	cima 5592	. . 3 class (𝑅 “ 𝐴)
5	4, 1	wss 3892	. 2 wff (𝑅 “ 𝐴) ⊆ 𝐴
6	3, 5	wb 205	1 wff (𝑅 hereditary 𝐴 ↔ (𝑅 “ 𝐴) ⊆ 𝐴)

This definition is referenced by:  dfhe2  41350  dfhe3  41351  heeq12  41352  sbcheg  41355  hess  41356  xphe  41357  0he  41358  he0  41360  unhe1  41361  snhesn  41362  dffrege76  41515