Theorem fndmdifcom

Description: The difference set between two functions is commutative. (Contributed by Stefan O'Rear, 17-Jan-2015)

	Ref	Expression
Assertion	fndmdifcom	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) → dom ( 𝐹 ∖ 𝐺 ) = dom ( 𝐺 ∖ 𝐹 ) )

Proof

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 ( 𝐺 ∖ 𝐹 ) )