Metamath Proof Explorer

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(RefRel{R}↔RefRel{S}\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}×\mathrm{ran}{R}=\mathrm{dom}{S}×\mathrm{ran}{S}$
4 3 ineq2d ${⊢}{R}={S}\to \mathrm{I}\cap \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)=\mathrm{I}\cap \left(\mathrm{dom}{S}×\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}×\mathrm{ran}{R}\right)\subseteq {R}↔\mathrm{I}\cap \left(\mathrm{dom}{S}×\mathrm{ran}{S}\right)\subseteq {S}\right)$
7 releq ${⊢}{R}={S}\to \left(\mathrm{Rel}{R}↔\mathrm{Rel}{S}\right)$
8 6 7 anbi12d ${⊢}{R}={S}\to \left(\left(\mathrm{I}\cap \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\wedge \mathrm{Rel}{R}\right)↔\left(\mathrm{I}\cap \left(\mathrm{dom}{S}×\mathrm{ran}{S}\right)\subseteq {S}\wedge \mathrm{Rel}{S}\right)\right)$
9 dfrefrel2 ${⊢}RefRel{R}↔\left(\mathrm{I}\cap \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\wedge \mathrm{Rel}{R}\right)$
10 dfrefrel2 ${⊢}RefRel{S}↔\left(\mathrm{I}\cap \left(\mathrm{dom}{S}×\mathrm{ran}{S}\right)\subseteq {S}\wedge \mathrm{Rel}{S}\right)$
11 8 9 10 3bitr4g ${⊢}{R}={S}\to \left(RefRel{R}↔RefRel{S}\right)$