Metamath Proof Explorer

Theorem imadif

Description: The image of a difference is the difference of images. (Contributed by NM, 24-May-1998)

Ref Expression
Assertion imadif 
|- ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) )

Proof

Step Hyp Ref Expression
1 anandir 
 |-  ( ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( ( x e. A /\ x F y ) /\ ( -. x e. B /\ x F y ) ) )
2 1 exbii 
 |-  ( E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> E. x ( ( x e. A /\ x F y ) /\ ( -. x e. B /\ x F y ) ) )
3 19.40 
 |-  ( E. x ( ( x e. A /\ x F y ) /\ ( -. x e. B /\ x F y ) ) -> ( E. x ( x e. A /\ x F y ) /\ E. x ( -. x e. B /\ x F y ) ) )
4 2 3 sylbi 
 |-  ( E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) -> ( E. x ( x e. A /\ x F y ) /\ E. x ( -. x e. B /\ x F y ) ) )
5 nfv 
 |-  F/ x Fun `' F
6 nfe1 
 |-  F/ x E. x ( x F y /\ -. x e. B )
7 5 6 nfan 
 |-  F/ x ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) )
8 funmo 
 |-  ( Fun `' F -> E* x y `' F x )
9 vex 
 |-  y e. _V
10 vex 
 |-  x e. _V
11 9 10 brcnv 
 |-  ( y `' F x <-> x F y )
12 11 mobii 
 |-  ( E* x y `' F x <-> E* x x F y )
13 8 12 sylib 
 |-  ( Fun `' F -> E* x x F y )
14 mopick 
 |-  ( ( E* x x F y /\ E. x ( x F y /\ -. x e. B ) ) -> ( x F y -> -. x e. B ) )
15 13 14 sylan 
 |-  ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> ( x F y -> -. x e. B ) )
16 15 con2d 
 |-  ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> ( x e. B -> -. x F y ) )
17 imnan 
 |-  ( ( x e. B -> -. x F y ) <-> -. ( x e. B /\ x F y ) )
18 16 17 sylib 
 |-  ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> -. ( x e. B /\ x F y ) )
19 7 18 alrimi 
 |-  ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> A. x -. ( x e. B /\ x F y ) )
20 19 ex 
 |-  ( Fun `' F -> ( E. x ( x F y /\ -. x e. B ) -> A. x -. ( x e. B /\ x F y ) ) )
21 exancom 
 |-  ( E. x ( x F y /\ -. x e. B ) <-> E. x ( -. x e. B /\ x F y ) )
22 alnex 
 |-  ( A. x -. ( x e. B /\ x F y ) <-> -. E. x ( x e. B /\ x F y ) )
23 20 21 22 3imtr3g 
 |-  ( Fun `' F -> ( E. x ( -. x e. B /\ x F y ) -> -. E. x ( x e. B /\ x F y ) ) )
24 23 anim2d 
 |-  ( Fun `' F -> ( ( E. x ( x e. A /\ x F y ) /\ E. x ( -. x e. B /\ x F y ) ) -> ( E. x ( x e. A /\ x F y ) /\ -. E. x ( x e. B /\ x F y ) ) ) )
25 4 24 syl5 
 |-  ( Fun `' F -> ( E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) -> ( E. x ( x e. A /\ x F y ) /\ -. E. x ( x e. B /\ x F y ) ) ) )
26 19.29r 
 |-  ( ( E. x ( x e. A /\ x F y ) /\ A. x -. ( x e. B /\ x F y ) ) -> E. x ( ( x e. A /\ x F y ) /\ -. ( x e. B /\ x F y ) ) )
27 22 26 sylan2br 
 |-  ( ( E. x ( x e. A /\ x F y ) /\ -. E. x ( x e. B /\ x F y ) ) -> E. x ( ( x e. A /\ x F y ) /\ -. ( x e. B /\ x F y ) ) )
28 andi 
 |-  ( ( ( x e. A /\ x F y ) /\ ( -. x e. B \/ -. x F y ) ) <-> ( ( ( x e. A /\ x F y ) /\ -. x e. B ) \/ ( ( x e. A /\ x F y ) /\ -. x F y ) ) )
29 ianor 
 |-  ( -. ( x e. B /\ x F y ) <-> ( -. x e. B \/ -. x F y ) )
30 29 anbi2i 
 |-  ( ( ( x e. A /\ x F y ) /\ -. ( x e. B /\ x F y ) ) <-> ( ( x e. A /\ x F y ) /\ ( -. x e. B \/ -. x F y ) ) )
31 an32 
 |-  ( ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( ( x e. A /\ x F y ) /\ -. x e. B ) )
32 pm3.24 
 |-  -. ( x F y /\ -. x F y )
33 32 intnan 
 |-  -. ( x e. A /\ ( x F y /\ -. x F y ) )
34 anass 
 |-  ( ( ( x e. A /\ x F y ) /\ -. x F y ) <-> ( x e. A /\ ( x F y /\ -. x F y ) ) )
35 33 34 mtbir 
 |-  -. ( ( x e. A /\ x F y ) /\ -. x F y )
36 35 biorfi 
 |-  ( ( ( x e. A /\ x F y ) /\ -. x e. B ) <-> ( ( ( x e. A /\ x F y ) /\ -. x e. B ) \/ ( ( x e. A /\ x F y ) /\ -. x F y ) ) )
37 31 36 bitri 
 |-  ( ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( ( ( x e. A /\ x F y ) /\ -. x e. B ) \/ ( ( x e. A /\ x F y ) /\ -. x F y ) ) )
38 28 30 37 3bitr4i 
 |-  ( ( ( x e. A /\ x F y ) /\ -. ( x e. B /\ x F y ) ) <-> ( ( x e. A /\ -. x e. B ) /\ x F y ) )
39 38 exbii 
 |-  ( E. x ( ( x e. A /\ x F y ) /\ -. ( x e. B /\ x F y ) ) <-> E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) )
40 27 39 sylib 
 |-  ( ( E. x ( x e. A /\ x F y ) /\ -. E. x ( x e. B /\ x F y ) ) -> E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) )
41 25 40 impbid1 
 |-  ( Fun `' F -> ( E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( E. x ( x e. A /\ x F y ) /\ -. E. x ( x e. B /\ x F y ) ) ) )
42 eldif 
 |-  ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
43 42 anbi1i 
 |-  ( ( x e. ( A \ B ) /\ x F y ) <-> ( ( x e. A /\ -. x e. B ) /\ x F y ) )
44 43 exbii 
 |-  ( E. x ( x e. ( A \ B ) /\ x F y ) <-> E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) )
45 9 elima2 
 |-  ( y e. ( F " A ) <-> E. x ( x e. A /\ x F y ) )
46 9 elima2 
 |-  ( y e. ( F " B ) <-> E. x ( x e. B /\ x F y ) )
47 46 notbii 
 |-  ( -. y e. ( F " B ) <-> -. E. x ( x e. B /\ x F y ) )
48 45 47 anbi12i 
 |-  ( ( y e. ( F " A ) /\ -. y e. ( F " B ) ) <-> ( E. x ( x e. A /\ x F y ) /\ -. E. x ( x e. B /\ x F y ) ) )
49 41 44 48 3bitr4g 
 |-  ( Fun `' F -> ( E. x ( x e. ( A \ B ) /\ x F y ) <-> ( y e. ( F " A ) /\ -. y e. ( F " B ) ) ) )
50 9 elima2 
 |-  ( y e. ( F " ( A \ B ) ) <-> E. x ( x e. ( A \ B ) /\ x F y ) )
51 eldif 
 |-  ( y e. ( ( F " A ) \ ( F " B ) ) <-> ( y e. ( F " A ) /\ -. y e. ( F " B ) ) )
52 49 50 51 3bitr4g 
 |-  ( Fun `' F -> ( y e. ( F " ( A \ B ) ) <-> y e. ( ( F " A ) \ ( F " B ) ) ) )
53 52 eqrdv 
 |-  ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) )