Metamath Proof Explorer

Theorem ereq1

Description: Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion ereq1 
|- ( R = S -> ( R Er A <-> S Er A ) )

Proof

Step Hyp Ref Expression
1 releq 
 |-  ( R = S -> ( Rel R <-> Rel S ) )
2 dmeq 
 |-  ( R = S -> dom R = dom S )
3 2 eqeq1d 
 |-  ( R = S -> ( dom R = A <-> dom S = A ) )
4 cnveq 
 |-  ( R = S -> `' R = `' S )
5 coeq1 
 |-  ( R = S -> ( R o. R ) = ( S o. R ) )
6 coeq2 
 |-  ( R = S -> ( S o. R ) = ( S o. S ) )
7 5 6 eqtrd 
 |-  ( R = S -> ( R o. R ) = ( S o. S ) )
8 4 7 uneq12d 
 |-  ( R = S -> ( `' R u. ( R o. R ) ) = ( `' S u. ( S o. S ) ) )
9 8 sseq1d 
 |-  ( R = S -> ( ( `' R u. ( R o. R ) ) C_ R <-> ( `' S u. ( S o. S ) ) C_ R ) )
10 sseq2 
 |-  ( R = S -> ( ( `' S u. ( S o. S ) ) C_ R <-> ( `' S u. ( S o. S ) ) C_ S ) )
11 9 10 bitrd 
 |-  ( R = S -> ( ( `' R u. ( R o. R ) ) C_ R <-> ( `' S u. ( S o. S ) ) C_ S ) )
12 1 3 11 3anbi123d 
 |-  ( R = S -> ( ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) <-> ( Rel S /\ dom S = A /\ ( `' S u. ( S o. S ) ) C_ S ) ) )
13 df-er 
 |-  ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ R ) )
14 df-er 
 |-  ( S Er A <-> ( Rel S /\ dom S = A /\ ( `' S u. ( S o. S ) ) C_ S ) )
15 12 13 14 3bitr4g 
 |-  ( R = S -> ( R Er A <-> S Er A ) )