Metamath Proof Explorer

Theorem heeq2

Description: Equality law for relations being herditary over a class. (Contributed by RP, 27-Mar-2020)

		Ref	Expression
	Assertion	heeq2	$⊢ A = B \to (R hereditary A \leftrightarrow R hereditary B)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ R = R$
2		heeq12	$⊢ (R = R \land A = B) \to (R hereditary A \leftrightarrow R hereditary B)$
3	1 2	mpan	$⊢ A = B \to (R hereditary A \leftrightarrow R hereditary B)$