Theorem imadif 5661

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

Assertion

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

Proof of Theorem imadif

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		anandir 827	. . . . . . . 8 |- ( ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( ( x e. A /\ x F y ) /\ ( -. x e. B /\ x F y ) ) )
2	1	exbii 1644	. . . . . . 7 |- ( 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 1656	. . . . . . 7 |- ( 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 195	. . . . . 6 |- ( 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 1683	. . . . . . . . . . 11 |- F/ x Fun `' F
6		nfe1 1789	. . . . . . . . . . 11 |- F/ x E. x ( x F y /\ -. x e. B )
7	5, 6	nfan 1875	. . . . . . . . . 10 |- F/ x ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) )
8		funmo 5602	. . . . . . . . . . . . . 14 |- ( Fun `' F -> E* x y `' F x )
9		vex 3116	. . . . . . . . . . . . . . . 16 |- y e. _V
10		vex 3116	. . . . . . . . . . . . . . . 16 |- x e. _V
11	9, 10	brcnv 5183	. . . . . . . . . . . . . . 15 |- ( y `' F x <-> x F y )
12	11	mobii 2301	. . . . . . . . . . . . . 14 |- ( E* x y `' F x <-> E* x x F y )
13	8, 12	sylib 196	. . . . . . . . . . . . 13 |- ( Fun `' F -> E* x x F y )
14		mopick 2361	. . . . . . . . . . . . 13 |- ( ( E* x x F y /\ E. x ( x F y /\ -. x e. B ) ) -> ( x F y -> -. x e. B ) )
15	13, 14	sylan 471	. . . . . . . . . . . 12 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> ( x F y -> -. x e. B ) )
16	15	con2d 115	. . . . . . . . . . 11 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> ( x e. B -> -. x F y ) )
17		imnan 422	. . . . . . . . . . 11 |- ( ( x e. B -> -. x F y ) <-> -. ( x e. B /\ x F y ) )
18	16, 17	sylib 196	. . . . . . . . . 10 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> -. ( x e. B /\ x F y ) )
19	7, 18	alrimi 1825	. . . . . . . . 9 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> A. x -. ( x e. B /\ x F y ) )
20	19	ex 434	. . . . . . . 8 |- ( Fun `' F -> ( E. x ( x F y /\ -. x e. B ) -> A. x -. ( x e. B /\ x F y ) ) )
21		exancom 1648	. . . . . . . 8 |- ( E. x ( x F y /\ -. x e. B ) <-> E. x ( -. x e. B /\ x F y ) )
22		alnex 1598	. . . . . . . 8 |- ( A. x -. ( x e. B /\ x F y ) <-> -. E. x ( x e. B /\ x F y ) )
23	20, 21, 22	3imtr3g 269	. . . . . . 7 |- ( Fun `' F -> ( E. x ( -. x e. B /\ x F y ) -> -. E. x ( x e. B /\ x F y ) ) )
24	23	anim2d 565	. . . . . 6 |- ( 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 32	. . . . 5 |- ( 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 1661	. . . . . . 7 |- ( ( 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 476	. . . . . 6 |- ( ( 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 865	. . . . . . . 8 |- ( ( ( 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 488	. . . . . . . . 9 |- ( -. ( x e. B /\ x F y ) <-> ( -. x e. B \/ -. x F y ) )
30	29	anbi2i 694	. . . . . . . 8 |- ( ( ( 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 796	. . . . . . . . 9 |- ( ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( ( x e. A /\ x F y ) /\ -. x e. B ) )
32		pm3.24 880	. . . . . . . . . . . 12 |- -. ( x F y /\ -. x F y )
33	32	intnan 912	. . . . . . . . . . 11 |- -. ( x e. A /\ ( x F y /\ -. x F y ) )
34		anass 649	. . . . . . . . . . 11 |- ( ( ( x e. A /\ x F y ) /\ -. x F y ) <-> ( x e. A /\ ( x F y /\ -. x F y ) ) )
35	33, 34	mtbir 299	. . . . . . . . . 10 |- -. ( ( x e. A /\ x F y ) /\ -. x F y )
36	35	biorfi 407	. . . . . . . . 9 |- ( ( ( 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 249	. . . . . . . 8 |- ( ( ( 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 277	. . . . . . 7 |- ( ( ( x e. A /\ x F y ) /\ -. ( x e. B /\ x F y ) ) <-> ( ( x e. A /\ -. x e. B ) /\ x F y ) )
39	38	exbii 1644	. . . . . 6 |- ( 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 196	. . . . 5 |- ( ( 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 203	. . . 4 |- ( 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 3486	. . . . . 6 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
43	42	anbi1i 695	. . . . 5 |- ( ( x e. ( A \ B ) /\ x F y ) <-> ( ( x e. A /\ -. x e. B ) /\ x F y ) )
44	43	exbii 1644	. . . 4 |- ( E. x ( x e. ( A \ B ) /\ x F y ) <-> E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) )
45	9	elima2 5341	. . . . 5 |- ( y e. ( F " A ) <-> E. x ( x e. A /\ x F y ) )
46	9	elima2 5341	. . . . . 6 |- ( y e. ( F " B ) <-> E. x ( x e. B /\ x F y ) )
47	46	notbii 296	. . . . 5 |- ( -. y e. ( F " B ) <-> -. E. x ( x e. B /\ x F y ) )
48	45, 47	anbi12i 697	. . . 4 |- ( ( 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 288	. . 3 |- ( Fun `' F -> ( E. x ( x e. ( A \ B ) /\ x F y ) <-> ( y e. ( F " A ) /\ -. y e. ( F " B ) ) ) )
50	9	elima2 5341	. . 3 |- ( y e. ( F " ( A \ B ) ) <-> E. x ( x e. ( A \ B ) /\ x F y ) )
51		eldif 3486	. . 3 |- ( y e. ( ( F " A ) \ ( F " B ) ) <-> ( y e. ( F " A ) /\ -. y e. ( F " B ) ) )
52	49, 50, 51	3bitr4g 288	. 2 |- ( Fun `' F -> ( y e. ( F " ( A \ B ) ) <-> y e. ( ( F " A ) \ ( F " B ) ) ) )
53	52	eqrdv 2464	1 |- ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   A.wal 1377   = wceq 1379   E.wex 1596   e. wcel 1767   E*wmo 2276   \ cdif 3473   class class class wbr 4447   `'ccnv 4998   "cima 5002   Fun wfun 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-fun 5588

This theorem is referenced by:  imain  5662  resdif  5834  difpreima  6007  domunsncan  7614  phplem4  7696  php3  7700  infdifsn  8069  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  mapfienOLD  8134  enfin1ai  8760  fin1a2lem7  8782  symgfixelsi  16252  dprdf1o  16866  frlmlbs  18595  f1lindf  18621  cnclima  19532  iscncl  19533  qtopcld  19946  qtoprest  19950  qtopcmap  19952  mbfimaicc  21772  ismbf3d  21793  i1fd  21820  ballotlemfrc  28102