Metamath Proof Explorer


Theorem heeq12

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

Ref Expression
Assertion heeq12 R = S A = B R hereditary A S hereditary B

Proof

Step Hyp Ref Expression
1 simpl R = S A = B R = S
2 simpr R = S A = B A = B
3 1 2 imaeq12d R = S A = B R A = S B
4 3 2 sseq12d R = S A = B R A A S B B
5 df-he R hereditary A R A A
6 df-he S hereditary B S B B
7 4 5 6 3bitr4g R = S A = B R hereditary A S hereditary B