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	$$⊢\varnothing hereditaryA$$

Proof

Step	Hyp	Ref	Expression
1		xphe	$$⊢\left(\varnothing \times A\right)hereditaryA$$
2		0xp	$$⊢\varnothing \times A=\varnothing$$
3		heeq1	$$⊢\varnothing \times A=\varnothing \to \left(\left(\varnothing \times A\right)hereditaryA\leftrightarrow \varnothing hereditaryA\right)$$
4	2 3	ax-mp	$$⊢\left(\varnothing \times A\right)hereditaryA\leftrightarrow \varnothing hereditaryA$$
5	1 4	mpbi	$$⊢\varnothing hereditaryA$$