| Step | Hyp | Ref | Expression | 
						
							| 1 |  | fdifsupp.1 |  |-  ( ph -> A e. V ) | 
						
							| 2 |  | fdifsupp.2 |  |-  ( ph -> Z e. W ) | 
						
							| 3 |  | fdifsupp.3 |  |-  ( ph -> F Fn A ) | 
						
							| 4 |  | difssd |  |-  ( ph -> ( A \ B ) C_ A ) | 
						
							| 5 | 3 4 | fnssresd |  |-  ( ph -> ( F |` ( A \ B ) ) Fn ( A \ B ) ) | 
						
							| 6 | 1 | difexd |  |-  ( ph -> ( A \ B ) e. _V ) | 
						
							| 7 |  | elsuppfn |  |-  ( ( ( F |` ( A \ B ) ) Fn ( A \ B ) /\ ( A \ B ) e. _V /\ Z e. W ) -> ( x e. ( ( F |` ( A \ B ) ) supp Z ) <-> ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) ) ) | 
						
							| 8 | 5 6 2 7 | syl3anc |  |-  ( ph -> ( x e. ( ( F |` ( A \ B ) ) supp Z ) <-> ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) ) ) | 
						
							| 9 |  | eldif |  |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) ) | 
						
							| 10 | 9 | anbi1i |  |-  ( ( x e. ( A \ B ) /\ ( F ` x ) =/= Z ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) ) | 
						
							| 11 | 10 | a1i |  |-  ( ph -> ( ( x e. ( A \ B ) /\ ( F ` x ) =/= Z ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) ) ) | 
						
							| 12 |  | simpr |  |-  ( ( ph /\ x e. ( A \ B ) ) -> x e. ( A \ B ) ) | 
						
							| 13 | 12 | fvresd |  |-  ( ( ph /\ x e. ( A \ B ) ) -> ( ( F |` ( A \ B ) ) ` x ) = ( F ` x ) ) | 
						
							| 14 | 13 | neeq1d |  |-  ( ( ph /\ x e. ( A \ B ) ) -> ( ( ( F |` ( A \ B ) ) ` x ) =/= Z <-> ( F ` x ) =/= Z ) ) | 
						
							| 15 | 14 | pm5.32da |  |-  ( ph -> ( ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) <-> ( x e. ( A \ B ) /\ ( F ` x ) =/= Z ) ) ) | 
						
							| 16 |  | an32 |  |-  ( ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) ) | 
						
							| 17 | 16 | a1i |  |-  ( ph -> ( ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) <-> ( ( x e. A /\ -. x e. B ) /\ ( F ` x ) =/= Z ) ) ) | 
						
							| 18 | 11 15 17 | 3bitr4d |  |-  ( ph -> ( ( x e. ( A \ B ) /\ ( ( F |` ( A \ B ) ) ` x ) =/= Z ) <-> ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) ) ) | 
						
							| 19 |  | eldif |  |-  ( x e. ( ( F supp Z ) \ B ) <-> ( x e. ( F supp Z ) /\ -. x e. B ) ) | 
						
							| 20 | 1 | elexd |  |-  ( ph -> A e. _V ) | 
						
							| 21 |  | elsuppfn |  |-  ( ( F Fn A /\ A e. _V /\ Z e. W ) -> ( x e. ( F supp Z ) <-> ( x e. A /\ ( F ` x ) =/= Z ) ) ) | 
						
							| 22 | 3 20 2 21 | syl3anc |  |-  ( ph -> ( x e. ( F supp Z ) <-> ( x e. A /\ ( F ` x ) =/= Z ) ) ) | 
						
							| 23 | 22 | anbi1d |  |-  ( ph -> ( ( x e. ( F supp Z ) /\ -. x e. B ) <-> ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) ) ) | 
						
							| 24 | 19 23 | bitr2id |  |-  ( ph -> ( ( ( x e. A /\ ( F ` x ) =/= Z ) /\ -. x e. B ) <-> x e. ( ( F supp Z ) \ B ) ) ) | 
						
							| 25 | 8 18 24 | 3bitrd |  |-  ( ph -> ( x e. ( ( F |` ( A \ B ) ) supp Z ) <-> x e. ( ( F supp Z ) \ B ) ) ) | 
						
							| 26 | 25 | eqrdv |  |-  ( ph -> ( ( F |` ( A \ B ) ) supp Z ) = ( ( F supp Z ) \ B ) ) |