Step 
Hyp 
Ref 
Expression 
1 

dflog2 
⊢ log = ^{◡} ( exp ↾ ran log ) 
2 
1

fveq1i 
⊢ ( log ‘ 𝐴 ) = ( ^{◡} ( exp ↾ ran log ) ‘ 𝐴 ) 
3 
2

fveq2i 
⊢ ( ( exp ↾ ran log ) ‘ ( log ‘ 𝐴 ) ) = ( ( exp ↾ ran log ) ‘ ( ^{◡} ( exp ↾ ran log ) ‘ 𝐴 ) ) 
4 

logrncl 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log ) 
5 
4

fvresd 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ↾ ran log ) ‘ ( log ‘ 𝐴 ) ) = ( exp ‘ ( log ‘ 𝐴 ) ) ) 
6 

eldifsn 
⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) 
7 

eff1o2 
⊢ ( exp ↾ ran log ) : ran log –11onto→ ( ℂ ∖ { 0 } ) 
8 

f1ocnvfv2 
⊢ ( ( ( exp ↾ ran log ) : ran log –11onto→ ( ℂ ∖ { 0 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( exp ↾ ran log ) ‘ ( ^{◡} ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 ) 
9 
7 8

mpan 
⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( ( exp ↾ ran log ) ‘ ( ^{◡} ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 ) 
10 
6 9

sylbir 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ↾ ran log ) ‘ ( ^{◡} ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 ) 
11 
3 5 10

3eqtr3a 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 ) 