Theorem 0he

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

	Ref	Expression
Assertion	0he	⊢ ∅ hereditary 𝐴

Proof

Step	Hyp	Ref	Expression
1		0ima	⊢ ( ∅ “ 𝐴 ) = ∅
2		0ss	⊢ ∅ ⊆ 𝐴
3	1 2	eqsstri	⊢ ( ∅ “ 𝐴 ) ⊆ 𝐴
4		df-he	⊢ ( ∅ hereditary 𝐴 ↔ ( ∅ “ 𝐴 ) ⊆ 𝐴 )
5	3 4	mpbir	⊢ ∅ hereditary 𝐴