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

syl6bb 
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) 