Theorem imadif 5676

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 836	. . . . . . . 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 1712	. . . . . . 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 1725	. . . . . . 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 198	. . . . . 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 1755	. . . . . . . . . . 11 |- F/ x Fun `' F
6		nfe1 1894	. . . . . . . . . . 11 |- F/ x E. x ( x F y /\ -. x e. B )
7	5, 6	nfan 1988	. . . . . . . . . 10 |- F/ x ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) )
8		funmo 5617	. . . . . . . . . . . . . 14 |- ( Fun `' F -> E* x y `' F x )
9		vex 3083	. . . . . . . . . . . . . . . 16 |- y e. _V
10		vex 3083	. . . . . . . . . . . . . . . 16 |- x e. _V
11	9, 10	brcnv 5036	. . . . . . . . . . . . . . 15 |- ( y `' F x <-> x F y )
12	11	mobii 2292	. . . . . . . . . . . . . 14 |- ( E* x y `' F x <-> E* x x F y )
13	8, 12	sylib 199	. . . . . . . . . . . . 13 |- ( Fun `' F -> E* x x F y )
14		mopick 2334	. . . . . . . . . . . . 13 |- ( ( E* x x F y /\ E. x ( x F y /\ -. x e. B ) ) -> ( x F y -> -. x e. B ) )
15	13, 14	sylan 473	. . . . . . . . . . . 12 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> ( x F y -> -. x e. B ) )
16	15	con2d 118	. . . . . . . . . . 11 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> ( x e. B -> -. x F y ) )
17		imnan 423	. . . . . . . . . . 11 |- ( ( x e. B -> -. x F y ) <-> -. ( x e. B /\ x F y ) )
18	16, 17	sylib 199	. . . . . . . . . 10 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> -. ( x e. B /\ x F y ) )
19	7, 18	alrimi 1932	. . . . . . . . 9 |- ( ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) ) -> A. x -. ( x e. B /\ x F y ) )
20	19	ex 435	. . . . . . . 8 |- ( Fun `' F -> ( E. x ( x F y /\ -. x e. B ) -> A. x -. ( x e. B /\ x F y ) ) )
21		exancom 1716	. . . . . . . 8 |- ( E. x ( x F y /\ -. x e. B ) <-> E. x ( -. x e. B /\ x F y ) )
22		alnex 1659	. . . . . . . 8 |- ( A. x -. ( x e. B /\ x F y ) <-> -. E. x ( x e. B /\ x F y ) )
23	20, 21, 22	3imtr3g 272	. . . . . . 7 |- ( Fun `' F -> ( E. x ( -. x e. B /\ x F y ) -> -. E. x ( x e. B /\ x F y ) ) )
24	23	anim2d 567	. . . . . 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 33	. . . . 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 1730	. . . . . . 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 478	. . . . . 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 875	. . . . . . . 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 490	. . . . . . . . 9 |- ( -. ( x e. B /\ x F y ) <-> ( -. x e. B \/ -. x F y ) )
30	29	anbi2i 698	. . . . . . . 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 805	. . . . . . . . 9 |- ( ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( ( x e. A /\ x F y ) /\ -. x e. B ) )
32		pm3.24 890	. . . . . . . . . . . 12 |- -. ( x F y /\ -. x F y )
33	32	intnan 922	. . . . . . . . . . 11 |- -. ( x e. A /\ ( x F y /\ -. x F y ) )
34		anass 653	. . . . . . . . . . 11 |- ( ( ( x e. A /\ x F y ) /\ -. x F y ) <-> ( x e. A /\ ( x F y /\ -. x F y ) ) )
35	33, 34	mtbir 300	. . . . . . . . . 10 |- -. ( ( x e. A /\ x F y ) /\ -. x F y )
36	35	biorfi 408	. . . . . . . . 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 252	. . . . . . . 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 280	. . . . . . 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 1712	. . . . . 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 199	. . . . 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 206	. . . 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 3446	. . . . . 6 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
43	42	anbi1i 699	. . . . 5 |- ( ( x e. ( A \ B ) /\ x F y ) <-> ( ( x e. A /\ -. x e. B ) /\ x F y ) )
44	43	exbii 1712	. . . 4 |- ( E. x ( x e. ( A \ B ) /\ x F y ) <-> E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) )
45	9	elima2 5193	. . . . 5 |- ( y e. ( F " A ) <-> E. x ( x e. A /\ x F y ) )
46	9	elima2 5193	. . . . . 6 |- ( y e. ( F " B ) <-> E. x ( x e. B /\ x F y ) )
47	46	notbii 297	. . . . 5 |- ( -. y e. ( F " B ) <-> -. E. x ( x e. B /\ x F y ) )
48	45, 47	anbi12i 701	. . . 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 291	. . 3 |- ( Fun `' F -> ( E. x ( x e. ( A \ B ) /\ x F y ) <-> ( y e. ( F " A ) /\ -. y e. ( F " B ) ) ) )
50	9	elima2 5193	. . 3 |- ( y e. ( F " ( A \ B ) ) <-> E. x ( x e. ( A \ B ) /\ x F y ) )
51		eldif 3446	. . 3 |- ( y e. ( ( F " A ) \ ( F " B ) ) <-> ( y e. ( F " A ) /\ -. y e. ( F " B ) ) )
52	49, 50, 51	3bitr4g 291	. 2 |- ( Fun `' F -> ( y e. ( F " ( A \ B ) ) <-> y e. ( ( F " A ) \ ( F " B ) ) ) )
53	52	eqrdv 2419	1 |- ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 369   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1657   e. wcel 1872   E*wmo 2270   \ cdif 3433   class class class wbr 4423   `'ccnv 4852   "cima 4856   Fun wfun 5595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-fun 5603

This theorem is referenced by:  imain  5677  resdif  5851  difpreima  6024  domunsncan  7682  phplem4  7764  php3  7768  infdifsn  8171  cantnfp1lem3  8194  enfin1ai  8822  fin1a2lem7  8844  symgfixelsi  17076  dprdf1o  17665  frlmlbs  19354  f1lindf  19379  cnclima  20283  iscncl  20284  qtopcld  20727  qtoprest  20731  qtopcmap  20733  mbfimaicc  22588  ismbf3d  22609  i1fd  22638  ballotlemfrc  29368  ballotlemfrcOLD  29406  poimirlem2  31907  poimirlem4  31909  poimirlem6  31911  poimirlem7  31912  poimirlem9  31914  poimirlem11  31916  poimirlem12  31917  poimirlem13  31918  poimirlem14  31919  poimirlem16  31921  poimirlem19  31924  poimirlem23  31928