Theorem heeq12

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

	Ref	Expression
Assertion	heeq12	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( 𝑅 hereditary 𝐴 ↔ 𝑆 hereditary 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → 𝑅 = 𝑆 )
2		simpr	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
3	1 2	imaeq12d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( 𝑅 “ 𝐴 ) = ( 𝑆 “ 𝐵 ) )
4	3 2	sseq12d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( ( 𝑅 “ 𝐴 ) ⊆ 𝐴 ↔ ( 𝑆 “ 𝐵 ) ⊆ 𝐵 ) )
5		df-he	⊢ ( 𝑅 hereditary 𝐴 ↔ ( 𝑅 “ 𝐴 ) ⊆ 𝐴 )
6		df-he	⊢ ( 𝑆 hereditary 𝐵 ↔ ( 𝑆 “ 𝐵 ) ⊆ 𝐵 )
7	4 5 6	3bitr4g	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( 𝑅 hereditary 𝐴 ↔ 𝑆 hereditary 𝐵 ) )