heeq12

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

		Ref	Expression
	Assertion	heeq12	$⊢ (R = S \land A = B) \to (R hereditary A \leftrightarrow S hereditary B)$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (R = S \land A = B) \to R = S$
2		simpr	$⊢ (R = S \land A = B) \to A = B$
3	1 2	imaeq12d	$⊢ (R = S \land A = B) \to R [A] = S [B]$
4	3 2	sseq12d	$⊢ (R = S \land A = B) \to (R [A] \subseteq A \leftrightarrow S [B] \subseteq B)$
5		df-he	$⊢ R hereditary A \leftrightarrow R [A] \subseteq A$
6		df-he	$⊢ S hereditary B \leftrightarrow S [B] \subseteq B$
7	4 5 6	3bitr4g	$⊢ (R = S \land A = B) \to (R hereditary A \leftrightarrow S hereditary B)$

Metamath Proof Explorer