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 -> ( RefRel R <-> RefRel S ) )

Proof

Step Hyp Ref Expression
1 dmeq 
 |-  ( R = S -> dom R = dom S )
2 rneq 
 |-  ( R = S -> ran R = ran S )
3 1 2 xpeq12d 
 |-  ( R = S -> ( dom R X. ran R ) = ( dom S X. ran S ) )
4 3 ineq2d 
 |-  ( R = S -> ( _I i^i ( dom R X. ran R ) ) = ( _I i^i ( dom S X. ran S ) ) )
5 id 
 |-  ( R = S -> R = S )
6 4 5 sseq12d 
 |-  ( R = S -> ( ( _I i^i ( dom R X. ran R ) ) C_ R <-> ( _I i^i ( dom S X. ran S ) ) C_ S ) )
7 releq 
 |-  ( R = S -> ( Rel R <-> Rel S ) )
8 6 7 anbi12d 
 |-  ( R = S -> ( ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) <-> ( ( _I i^i ( dom S X. ran S ) ) C_ S /\ Rel S ) ) )
9 dfrefrel2 
 |-  ( RefRel R <-> ( ( _I i^i ( dom R X. ran R ) ) C_ R /\ Rel R ) )
10 dfrefrel2 
 |-  ( RefRel S <-> ( ( _I i^i ( dom S X. ran S ) ) C_ S /\ Rel S ) )
11 8 9 10 3bitr4g 
 |-  ( R = S -> ( RefRel R <-> RefRel S ) )