This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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