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

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 ⊢ Ⅎ 𝑥 𝐹
eqfnfv2f.2 ⊢ Ⅎ 𝑥 𝐺
Assertion eqfnfv2f ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 eqfnfv2f.1 ⊢ Ⅎ 𝑥 𝐹
2 eqfnfv2f.2 ⊢ Ⅎ 𝑥 𝐺
3 eqfnfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) )
4 nfcv ⊢ Ⅎ 𝑥 𝑧
5 1 4 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
6 2 4 nffv ⊢ Ⅎ 𝑥 ( 𝐺 ‘ 𝑧 )
7 5 6 nfeq ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 )
8 nfv ⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 )
9 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
10 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑥 ) )
11 9 10 eqeq12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
12 7 8 11 cbvralw ⊢ ( ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
13 3 12 bitrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )