Theorem 0heALT

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

	Ref	Expression
Assertion	0heALT	⊢ ∅ hereditary 𝐴

Proof

Step	Hyp	Ref	Expression
1		xphe	⊢ ( ∅ × 𝐴 ) hereditary 𝐴
2		0xp	⊢ ( ∅ × 𝐴 ) = ∅
3		heeq1	⊢ ( ( ∅ × 𝐴 ) = ∅ → ( ( ∅ × 𝐴 ) hereditary 𝐴 ↔ ∅ hereditary 𝐴 ) )
4	2 3	ax-mp	⊢ ( ( ∅ × 𝐴 ) hereditary 𝐴 ↔ ∅ hereditary 𝐴 )
5	1 4	mpbi	⊢ ∅ hereditary 𝐴