This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqfnfvd

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

Ref Expression
Hypotheses eqfnfvd.1 ⊢ φ → F Fn A
eqfnfvd.2 ⊢ φ → G Fn A
eqfnfvd.3 ⊢ φ ∧ x ∈ A → F ⁡ x = G ⁡ x
Assertion eqfnfvd ⊢ φ → F = G

Proof

Step Hyp Ref Expression
1 eqfnfvd.1 ⊢ φ → F Fn A
2 eqfnfvd.2 ⊢ φ → G Fn A
3 eqfnfvd.3 ⊢ φ ∧ x ∈ A → F ⁡ x = G ⁡ x
4 3 ralrimiva ⊢ φ → ∀ x ∈ A F ⁡ x = G ⁡ x
5 eqfnfv ⊢ F Fn A ∧ G Fn A → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
6 1 2 5 syl2anc ⊢ φ → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
7 4 6 mpbird ⊢ φ → F = G