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 ) C_ A <-> ( S " B ) C_ B ) )
5		df-he	|- ( R hereditary A <-> ( R " A ) C_ A )
6		df-he	|- ( S hereditary B <-> ( S " B ) C_ B )
7	4 5 6	3bitr4g	|- ( ( R = S /\ A = B ) -> ( R hereditary A <-> S hereditary B ) )