Step 
Hyp 
Ref 
Expression 
1 

necom 
⊢ ( ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑥 ) ) 
2 
1

rabbii 
⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) } = { 𝑥 ∈ 𝐴 ∣ ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑥 ) } 
3 

fndmdif 
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∖ 𝐺 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐺 ‘ 𝑥 ) } ) 
4 

fndmdif 
⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) → dom ( 𝐺 ∖ 𝐹 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑥 ) } ) 
5 
4

ancoms 
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐺 ∖ 𝐹 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝐺 ‘ 𝑥 ) ≠ ( 𝐹 ‘ 𝑥 ) } ) 
6 
2 3 5

3eqtr4a 
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∖ 𝐺 ) = dom ( 𝐺 ∖ 𝐹 ) ) 