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 e. A | ( F ` x ) =/= ( G ` x ) } = { x e. A | ( G ` x ) =/= ( F ` x ) }
3		fndmdif	|- ( ( F Fn A /\ G Fn A ) -> dom ( F \ G ) = { x e. A | ( F ` x ) =/= ( G ` x ) } )
4		fndmdif	|- ( ( G Fn A /\ F Fn A ) -> dom ( G \ F ) = { x e. A | ( G ` x ) =/= ( F ` x ) } )
5	4	ancoms	|- ( ( F Fn A /\ G Fn A ) -> dom ( G \ F ) = { x e. A | ( G ` x ) =/= ( F ` x ) } )
6	2 3 5	3eqtr4a	|- ( ( F Fn A /\ G Fn A ) -> dom ( F \ G ) = dom ( G \ F ) )