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 ⊢ F Fn A ∧ G Fn A → dom ⁡ F ∖ G = dom ⁡ G ∖ F

Proof

Step Hyp Ref Expression
1 necom ⊢ F ⁡ x ≠ G ⁡ x ↔ G ⁡ x ≠ F ⁡ x
2 1 rabbii ⊢ x ∈ A | F ⁡ x ≠ G ⁡ x = x ∈ A | G ⁡ x ≠ F ⁡ x
3 fndmdif ⊢ F Fn A ∧ G Fn A → dom ⁡ F ∖ G = x ∈ A | F ⁡ x ≠ G ⁡ x
4 fndmdif ⊢ G Fn A ∧ F Fn A → dom ⁡ G ∖ F = x ∈ A | G ⁡ x ≠ F ⁡ x
5 4 ancoms ⊢ F Fn A ∧ G Fn A → dom ⁡ G ∖ F = x ∈ A | G ⁡ x ≠ F ⁡ x
6 2 3 5 3eqtr4a ⊢ F Fn A ∧ G Fn A → dom ⁡ F ∖ G = dom ⁡ G ∖ F