This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Equality theorem for functions. (Contributed by FL, 14-Jul-2007) (Proof
shortened by Andrew Salmon, 17-Sep-2011)
|
|
Ref |
Expression |
|
Assertion |
feq23 |
⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐷 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
feq2 |
⊢ ( 𝐴 = 𝐶 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐵 ) ) |
| 2 |
|
feq3 |
⊢ ( 𝐵 = 𝐷 → ( 𝐹 : 𝐶 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐷 ) ) |
| 3 |
1 2
|
sylan9bb |
⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐶 ⟶ 𝐷 ) ) |