Step |
Hyp |
Ref |
Expression |
1 |
|
coeq1 |
⊢ ( 𝐹 = 𝐺 → ( 𝐹 ∘ 2nd ) = ( 𝐺 ∘ 2nd ) ) |
2 |
|
frecseq123 |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ ( 𝐹 ∘ 2nd ) = ( 𝐺 ∘ 2nd ) ) → frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2nd ) ) ) |
3 |
1 2
|
syl3an3 |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2nd ) ) ) |
4 |
|
df-wrecs |
⊢ wrecs ( 𝑅 , 𝐴 , 𝐹 ) = frecs ( 𝑅 , 𝐴 , ( 𝐹 ∘ 2nd ) ) |
5 |
|
df-wrecs |
⊢ wrecs ( 𝑆 , 𝐵 , 𝐺 ) = frecs ( 𝑆 , 𝐵 , ( 𝐺 ∘ 2nd ) ) |
6 |
3 4 5
|
3eqtr4g |
⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺 ) → wrecs ( 𝑅 , 𝐴 , 𝐹 ) = wrecs ( 𝑆 , 𝐵 , 𝐺 ) ) |