**Description:** Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref | Expression | ||
---|---|---|---|

Hypotheses | eqfnfvd.1 | ⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) | |

eqfnfvd.2 | ⊢ ( 𝜑 → 𝐺 Fn 𝐴 ) | ||

eqfnfvd.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) | ||

Assertion | eqfnfvd | ⊢ ( 𝜑 → 𝐹 = 𝐺 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eqfnfvd.1 | ⊢ ( 𝜑 → 𝐹 Fn 𝐴 ) | |

2 | eqfnfvd.2 | ⊢ ( 𝜑 → 𝐺 Fn 𝐴 ) | |

3 | eqfnfvd.3 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) | |

4 | 3 | ralrimiva | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |

5 | eqfnfv | ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) | |

6 | 1 2 5 | syl2anc | ⊢ ( 𝜑 → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) |

7 | 4 6 | mpbird | ⊢ ( 𝜑 → 𝐹 = 𝐺 ) |