Theorem 0he

Description: The empty relation is hereditary in any class. (Contributed by RP, 27-Mar-2020)

	Ref	Expression
Assertion	0he	$$⊢\varnothing hereditaryA$$

Proof

Step	Hyp	Ref	Expression
1		0ima	$$⊢\varnothing \left[A\right]=\varnothing$$
2		0ss	$$⊢\varnothing \subseteq A$$
3	1 2	eqsstri	$$⊢\varnothing \left[A\right]\subseteq A$$
4		df-he	$$⊢\varnothing hereditaryA\leftrightarrow \varnothing \left[A\right]\subseteq A$$
5	3 4	mpbir	$$⊢\varnothing hereditaryA$$