Theorem he0

Description: Any relation is hereditary in the empty set. (Contributed by RP, 27-Mar-2020)

	Ref	Expression
Assertion	he0	$$⊢Ahereditary\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		ima0	$$⊢A\left[\varnothing \right]=\varnothing$$
2	1	eqimssi	$$⊢A\left[\varnothing \right]\subseteq \varnothing$$
3		df-he	$$⊢Ahereditary\varnothing \leftrightarrow A\left[\varnothing \right]\subseteq \varnothing$$
4	2 3	mpbir	$$⊢Ahereditary\varnothing$$