Theorem he0

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

	Ref	Expression
Assertion	he0	⊢ 𝐴 hereditary ∅

Proof

Step	Hyp	Ref	Expression
1		ima0	⊢ ( 𝐴 “ ∅ ) = ∅
2	1	eqimssi	⊢ ( 𝐴 “ ∅ ) ⊆ ∅
3		df-he	⊢ ( 𝐴 hereditary ∅ ↔ ( 𝐴 “ ∅ ) ⊆ ∅ )
4	2 3	mpbir	⊢ 𝐴 hereditary ∅