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 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 ) )