Theorem dfhe2

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

	Ref	Expression
Assertion	dfhe2	$$⊢RhereditaryA\leftrightarrow {R\upharpoonright }_A\subseteq A\times A$$

Proof

Step	Hyp	Ref	Expression
1		df-he	$$⊢RhereditaryA\leftrightarrow R\left[A\right]\subseteq A$$
2		resssxp	$$⊢R\left[A\right]\subseteq A\leftrightarrow {R\upharpoonright }_A\subseteq A\times A$$
3	1 2	bitri	$$⊢RhereditaryA\leftrightarrow {R\upharpoonright }_A\subseteq A\times A$$