Description: Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | imbrov2fvoveq.1 | ⊢ ( 𝑋 = 𝑌 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | imbrov2fvoveq | ⊢ ( 𝑋 = 𝑌 → ( ( 𝜑 → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑋 ) · 𝑂 ) ) 𝑅 𝐴 ) ↔ ( 𝜓 → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑌 ) · 𝑂 ) ) 𝑅 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imbrov2fvoveq.1 | ⊢ ( 𝑋 = 𝑌 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | fveq2 | ⊢ ( 𝑋 = 𝑌 → ( 𝐺 ‘ 𝑋 ) = ( 𝐺 ‘ 𝑌 ) ) | |
| 3 | 2 | fvoveq1d | ⊢ ( 𝑋 = 𝑌 → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑋 ) · 𝑂 ) ) = ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑌 ) · 𝑂 ) ) ) |
| 4 | 3 | breq1d | ⊢ ( 𝑋 = 𝑌 → ( ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑋 ) · 𝑂 ) ) 𝑅 𝐴 ↔ ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑌 ) · 𝑂 ) ) 𝑅 𝐴 ) ) |
| 5 | 1 4 | imbi12d | ⊢ ( 𝑋 = 𝑌 → ( ( 𝜑 → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑋 ) · 𝑂 ) ) 𝑅 𝐴 ) ↔ ( 𝜓 → ( 𝐹 ‘ ( ( 𝐺 ‘ 𝑌 ) · 𝑂 ) ) 𝑅 𝐴 ) ) ) |