Step 
Hyp 
Ref 
Expression 
1 

funrel 
⊢ ( Fun 𝐹 → Rel 𝐹 ) 
2 

brrelex2 
⊢ ( ( Rel 𝐹 ∧ 𝐴 𝐹 𝐵 ) → 𝐵 ∈ V ) 
3 
1 2

sylan 
⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → 𝐵 ∈ V ) 
4 

breq2 
⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐹 𝑦 ↔ 𝐴 𝐹 𝐵 ) ) 
5 
4

anbi2d 
⊢ ( 𝑦 = 𝐵 → ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝑦 ) ↔ ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) ) ) 
6 

eqeq2 
⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) = 𝑦 ↔ ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ) 
7 
5 6

imbi12d 
⊢ ( 𝑦 = 𝐵 → ( ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝑦 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 ) ↔ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ) ) 
8 

funeu 
⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝑦 ) → ∃! 𝑦 𝐴 𝐹 𝑦 ) 
9 

tz6.121 
⊢ ( ( 𝐴 𝐹 𝑦 ∧ ∃! 𝑦 𝐴 𝐹 𝑦 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 ) 
10 
8 9

sylan2 
⊢ ( ( 𝐴 𝐹 𝑦 ∧ ( Fun 𝐹 ∧ 𝐴 𝐹 𝑦 ) ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 ) 
11 
10

anabss7 
⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝑦 ) → ( 𝐹 ‘ 𝐴 ) = 𝑦 ) 
12 
7 11

vtoclg 
⊢ ( 𝐵 ∈ V → ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ) 
13 
3 12

mpcom 
⊢ ( ( Fun 𝐹 ∧ 𝐴 𝐹 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) 
14 
13

ex 
⊢ ( Fun 𝐹 → ( 𝐴 𝐹 𝐵 → ( 𝐹 ‘ 𝐴 ) = 𝐵 ) ) 