Theorem refreleq

Description: Equality theorem for reflexive relation. (Contributed by Peter Mazsa, 15-Apr-2019) (Revised by Peter Mazsa, 23-Sep-2021)

	Ref	Expression
Assertion	refreleq	$$⊢R=S\to \left(RefRelR\leftrightarrow RefRelS\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmeq	$$⊢R=S\to \mathrm{dom}R=\mathrm{dom}S$$
2		rneq	$$⊢R=S\to \mathrm{ran}R=\mathrm{ran}S$$
3	1 2	xpeq12d	$$⊢R=S\to \mathrm{dom}R\times \mathrm{ran}R=\mathrm{dom}S\times \mathrm{ran}S$$
4	3	ineq2d	$$⊢R=S\to \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)=\mathrm{I}\cap \left(\mathrm{dom}S\times \mathrm{ran}S\right)$$
5		id	$$⊢R=S\to R=S$$
6	4 5	sseq12d	$$⊢R=S\to \left(\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\leftrightarrow \mathrm{I}\cap \left(\mathrm{dom}S\times \mathrm{ran}S\right)\subseteq S\right)$$
7		releq	$$⊢R=S\to \left(\mathrm{Rel}R\leftrightarrow \mathrm{Rel}S\right)$$
8	6 7	anbi12d	$$⊢R=S\to \left(\left(\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\wedge \mathrm{Rel}R\right)\leftrightarrow \left(\mathrm{I}\cap \left(\mathrm{dom}S\times \mathrm{ran}S\right)\subseteq S\wedge \mathrm{Rel}S\right)\right)$$
9		dfrefrel2	$$⊢RefRelR\leftrightarrow \left(\mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq R\wedge \mathrm{Rel}R\right)$$
10		dfrefrel2	$$⊢RefRelS\leftrightarrow \left(\mathrm{I}\cap \left(\mathrm{dom}S\times \mathrm{ran}S\right)\subseteq S\wedge \mathrm{Rel}S\right)$$
11	8 9 10	3bitr4g	$$⊢R=S\to \left(RefRelR\leftrightarrow RefRelS\right)$$