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	$$⊢RhereditaryA\leftrightarrow R\left[A\right]\subseteq A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	whe	$$wffRhereditaryA$$
3	0 1	cima	$$classR\left[A\right]$$
4	3 1	wss	$$wffR\left[A\right]\subseteq A$$
5	2 4	wb	$$wff\left(RhereditaryA\leftrightarrow R\left[A\right]\subseteq A\right)$$