Step |
Hyp |
Ref |
Expression |
1 |
|
coeq1 |
|- ( F = G -> ( F o. 2nd ) = ( G o. 2nd ) ) |
2 |
|
frecseq123 |
|- ( ( R = S /\ A = B /\ ( F o. 2nd ) = ( G o. 2nd ) ) -> frecs ( R , A , ( F o. 2nd ) ) = frecs ( S , B , ( G o. 2nd ) ) ) |
3 |
1 2
|
syl3an3 |
|- ( ( R = S /\ A = B /\ F = G ) -> frecs ( R , A , ( F o. 2nd ) ) = frecs ( S , B , ( G o. 2nd ) ) ) |
4 |
|
df-wrecs |
|- wrecs ( R , A , F ) = frecs ( R , A , ( F o. 2nd ) ) |
5 |
|
df-wrecs |
|- wrecs ( S , B , G ) = frecs ( S , B , ( G o. 2nd ) ) |
6 |
3 4 5
|
3eqtr4g |
|- ( ( R = S /\ A = B /\ F = G ) -> wrecs ( R , A , F ) = wrecs ( S , B , G ) ) |