Step 
Hyp 
Ref 
Expression 
1 

isomushgr.v 
⊢ 𝑉 = ( Vtx ‘ 𝐴 ) 
2 

isomushgr.w 
⊢ 𝑊 = ( Vtx ‘ 𝐵 ) 
3 

isomushgr.e 
⊢ 𝐸 = ( Edg ‘ 𝐴 ) 
4 

isomushgr.k 
⊢ 𝐾 = ( Edg ‘ 𝐵 ) 
5 

isomuspgrlem2.g 
⊢ 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) 
6 
5

a1i 
⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → 𝐺 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ) 
7 

imaeq2 
⊢ ( 𝑥 = 𝑒 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑒 ) ) 
8 
7

adantl 
⊢ ( ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑥 = 𝑒 ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑒 ) ) 
9 

simpr 
⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 ) 
10 

imaexg 
⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 “ 𝑒 ) ∈ V ) 
11 
10

adantr 
⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → ( 𝐹 “ 𝑒 ) ∈ V ) 
12 
6 8 9 11

fvmptd 
⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → ( 𝐺 ‘ 𝑒 ) = ( 𝐹 “ 𝑒 ) ) 
13 
12

eqcomd 
⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑒 ∈ 𝐸 ) → ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) 
14 
13

ralrimiva 
⊢ ( 𝐹 ∈ 𝑋 → ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) 