Theorem imadif 5669

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 829	. . . . . . . 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 1668	. . . . . . 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 1680	. . . . . . 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 1708	. . . . . . . . . . 11 |- F/ x Fun `' F
6		nfe1 1841	. . . . . . . . . . 11 |- F/ x E. x ( x F y /\ -. x e. B )
7	5, 6	nfan 1929	. . . . . . . . . 10 |- F/ x ( Fun `' F /\ E. x ( x F y /\ -. x e. B ) )
8		funmo 5610	. . . . . . . . . . . . . 14 |- ( Fun `' F -> E* x y `' F x )
9		vex 3112	. . . . . . . . . . . . . . . 16 |- y e. _V
10		vex 3112	. . . . . . . . . . . . . . . 16 |- x e. _V
11	9, 10	brcnv 5195	. . . . . . . . . . . . . . 15 |- ( y `' F x <-> x F y )
12	11	mobii 2308	. . . . . . . . . . . . . 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 2356	. . . . . . . . . . . . 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 1878	. . . . . . . . 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 1672	. . . . . . . 8 |- ( E. x ( x F y /\ -. x e. B ) <-> E. x ( -. x e. B /\ x F y ) )
22		alnex 1615	. . . . . . . 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 1685	. . . . . . 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 867	. . . . . . . 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 798	. . . . . . . . 9 |- ( ( ( x e. A /\ -. x e. B ) /\ x F y ) <-> ( ( x e. A /\ x F y ) /\ -. x e. B ) )
32		pm3.24 882	. . . . . . . . . . . 12 |- -. ( x F y /\ -. x F y )
33	32	intnan 914	. . . . . . . . . . 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 1668	. . . . . 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 3481	. . . . . 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 1668	. . . 4 |- ( E. x ( x e. ( A \ B ) /\ x F y ) <-> E. x ( ( x e. A /\ -. x e. B ) /\ x F y ) )
45	9	elima2 5353	. . . . 5 |- ( y e. ( F " A ) <-> E. x ( x e. A /\ x F y ) )
46	9	elima2 5353	. . . . . 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 5353	. . 3 |- ( y e. ( F " ( A \ B ) ) <-> E. x ( x e. ( A \ B ) /\ x F y ) )
51		eldif 3481	. . 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 2454	1 |- ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 368   /\ wa 369   A.wal 1393   = wceq 1395   E.wex 1613   e. wcel 1819   E*wmo 2284   \ cdif 3468   class class class wbr 4456   `'ccnv 5007   "cima 5011   Fun wfun 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-fun 5596

This theorem is referenced by:  imain  5670  resdif  5842  difpreima  6016  domunsncan  7636  phplem4  7718  php3  7722  infdifsn  8090  cantnfp1lem3  8116  cantnfp1lem3OLD  8142  mapfienOLD  8155  enfin1ai  8781  fin1a2lem7  8803  symgfixelsi  16586  dprdf1o  17205  frlmlbs  18957  f1lindf  18983  cnclima  19895  iscncl  19896  qtopcld  20339  qtoprest  20343  qtopcmap  20345  mbfimaicc  22165  ismbf3d  22186  i1fd  22213  ballotlemfrc  28640