Metamath Proof Explorer

Theorem eqfnfv2f

Description: Equality of functions is determined by their values. Special case of Exercise 4 of TakeutiZaring p. 28 (with domain equality omitted). This version of eqfnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004)

Ref Expression
Hypotheses eqfnfv2f.1 ⊢ Ⅎ _ x F
eqfnfv2f.2 ⊢ Ⅎ _ x G
Assertion eqfnfv2f ⊢ F Fn A ∧ G Fn A → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x

Proof

Step Hyp Ref Expression
1 eqfnfv2f.1 ⊢ Ⅎ _ x F
2 eqfnfv2f.2 ⊢ Ⅎ _ x G
3 eqfnfv ⊢ F Fn A ∧ G Fn A → F = G ↔ ∀ z ∈ A F ⁡ z = G ⁡ z
4 nfcv ⊢ Ⅎ _ x z
5 1 4 nffv ⊢ Ⅎ _ x F ⁡ z
6 2 4 nffv ⊢ Ⅎ _ x G ⁡ z
7 5 6 nfeq ⊢ Ⅎ x F ⁡ z = G ⁡ z
8 nfv ⊢ Ⅎ z F ⁡ x = G ⁡ x
9 fveq2 ⊢ z = x → F ⁡ z = F ⁡ x
10 fveq2 ⊢ z = x → G ⁡ z = G ⁡ x
11 9 10 eqeq12d ⊢ z = x → F ⁡ z = G ⁡ z ↔ F ⁡ x = G ⁡ x
12 7 8 11 cbvralw ⊢ ∀ z ∈ A F ⁡ z = G ⁡ z ↔ ∀ x ∈ A F ⁡ x = G ⁡ x
13 3 12 bitrdi ⊢ F Fn A ∧ G Fn A → F = G ↔ ∀ x ∈ A F ⁡ x = G ⁡ x