Theorem imadif 2714

Description: The image of a difference is the difference of images.

Assertion

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

Proof of Theorem imadif

Step	Hyp	Ref	Expression
1		ax-17 925	. . . . . . . . . . 11 |- (Fun `'F -> A.xFun `'F)
2		hbe1 709	. . . . . . . . . . 11 |- (E.x(xFy /\ -. x e. B) -> A.xE.x(xFy /\ -. x e. B))
3	1, 2	hban 704	. . . . . . . . . 10 |- ((Fun `'F /\ E.x(xFy /\ -. x e. B)) -> A.x(Fun `'F /\ E.x(xFy /\ -. x e. B)))
4		mopick 1054	. . . . . . . . . . . . 13 |- ((E*x xFy /\ E.x(xFy /\ -. x e. B)) -> (xFy -> -. x e. B))
5		funmo 2680	. . . . . . . . . . . . . 14 |- (Fun `'F -> E*x y`'Fx)
6		visset 1350	. . . . . . . . . . . . . . . 16 |- y e. V
7		visset 1350	. . . . . . . . . . . . . . . 16 |- x e. V
8	6, 7	brcnv 2519	. . . . . . . . . . . . . . 15 |- (y`'Fx <-> xFy)
9	8	bimo 1031	. . . . . . . . . . . . . 14 |- (E*x y`'Fx <-> E*x xFy)
10	5, 9	sylib 173	. . . . . . . . . . . . 13 |- (Fun `'F -> E*x xFy)
11	4, 10	sylan 343	. . . . . . . . . . . 12 |- ((Fun `'F /\ E.x(xFy /\ -. x e. B)) -> (xFy -> -. x e. B))
12	11	con2d 83	. . . . . . . . . . 11 |- ((Fun `'F /\ E.x(xFy /\ -. x e. B)) -> (x e. B -> -. xFy))
13		imnan 207	. . . . . . . . . . 11 |- ((x e. B -> -. xFy) <-> -. (x e. B /\ xFy))
14	12, 13	sylib 173	. . . . . . . . . 10 |- ((Fun `'F /\ E.x(xFy /\ -. x e. B)) -> -. (x e. B /\ xFy))
15	3, 14	19.21ai 740	. . . . . . . . 9 |- ((Fun `'F /\ E.x(xFy /\ -. x e. B)) -> A.x -. (x e. B /\ xFy))
16	15	exp 291	. . . . . . . 8 |- (Fun `'F -> (E.x(xFy /\ -. x e. B) -> A.x -. (x e. B /\ xFy)))
17		exancom 736	. . . . . . . 8 |- (E.x(xFy /\ -. x e. B) <-> E.x(-. x e. B /\ xFy))
18		alnex 716	. . . . . . . 8 |- (A.x -. (x e. B /\ xFy) <-> -. E.x(x e. B /\ xFy))
19	16, 17, 18	3imtr3g 425	. . . . . . 7 |- (Fun `'F -> (E.x(-. x e. B /\ xFy) -> -. E.x(x e. B /\ xFy)))
20	19	anim2d 433	. . . . . 6 |- (Fun `'F -> ((E.x(x e. A /\ xFy) /\ E.x(-. x e. B /\ xFy)) -> (E.x(x e. A /\ xFy) /\ -. E.x(x e. B /\ xFy))))
21		anandir 393	. . . . . . . 8 |- (((x e. A /\ -. x e. B) /\ xFy) <-> ((x e. A /\ xFy) /\ (-. x e. B /\ xFy)))
22	21	biex 733	. . . . . . 7 |- (E.x((x e. A /\ -. x e. B) /\ xFy) <-> E.x((x e. A /\ xFy) /\ (-. x e. B /\ xFy)))
23		19.40 773	. . . . . . 7 |- (E.x((x e. A /\ xFy) /\ (-. x e. B /\ xFy)) -> (E.x(x e. A /\ xFy) /\ E.x(-. x e. B /\ xFy)))
24	22, 23	sylbi 174	. . . . . 6 |- (E.x((x e. A /\ -. x e. B) /\ xFy) -> (E.x(x e. A /\ xFy) /\ E.x(-. x e. B /\ xFy)))
25	20, 24	syl5 22	. . . . 5 |- (Fun `'F -> (E.x((x e. A /\ -. x e. B) /\ xFy) -> (E.x(x e. A /\ xFy) /\ -. E.x(x e. B /\ xFy))))
26		19.29r 753	. . . . . . . 8 |- ((E.x(x e. A /\ xFy) /\ A.x -. (x e. B /\ xFy)) -> E.x((x e. A /\ xFy) /\ -. (x e. B /\ xFy)))
27	26, 18	sylan2br 348	. . . . . . 7 |- ((E.x(x e. A /\ xFy) /\ -. E.x(x e. B /\ xFy)) -> E.x((x e. A /\ xFy) /\ -. (x e. B /\ xFy)))
28		andi 456	. . . . . . . . 9 |- (((x e. A /\ xFy) /\ (-. x e. B \/ -. xFy)) <-> (((x e. A /\ xFy) /\ -. x e. B) \/ ((x e. A /\ xFy) /\ -. xFy)))
29		ianor 253	. . . . . . . . . 10 |- (-. (x e. B /\ xFy) <-> (-. x e. B \/ -. xFy))
30	29	anbi2i 367	. . . . . . . . 9 |- (((x e. A /\ xFy) /\ -. (x e. B /\ xFy)) <-> ((x e. A /\ xFy) /\ (-. x e. B \/ -. xFy)))
31		an23 371	. . . . . . . . . 10 |- (((x e. A /\ -. x e. B) /\ xFy) <-> ((x e. A /\ xFy) /\ -. x e. B))
32		pm3.24 496	. . . . . . . . . . . . 13 |- -. (xFy /\ -. xFy)
33	32	intnan 516	. . . . . . . . . . . 12 |- -. (x e. A /\ (xFy /\ -. xFy))
34		anass 336	. . . . . . . . . . . 12 |- (((x e. A /\ xFy) /\ -. xFy) <-> (x e. A /\ (xFy /\ -. xFy)))
35	33, 34	mtbir 167	. . . . . . . . . . 11 |- -. ((x e. A /\ xFy) /\ -. xFy)
36	35	biorfi 552	. . . . . . . . . 10 |- (((x e. A /\ xFy) /\ -. x e. B) <-> (((x e. A /\ xFy) /\ -. x e. B) \/ ((x e. A /\ xFy) /\ -. xFy)))
37	31, 36	bitr 151	. . . . . . . . 9 |- (((x e. A /\ -. x e. B) /\ xFy) <-> (((x e. A /\ xFy) /\ -. x e. B) \/ ((x e. A /\ xFy) /\ -. xFy)))
38	28, 30, 37	3bitr4 158	. . . . . . . 8 |- (((x e. A /\ xFy) /\ -. (x e. B /\ xFy)) <-> ((x e. A /\ -. x e. B) /\ xFy))
39	38	biex 733	. . . . . . 7 |- (E.x((x e. A /\ xFy) /\ -. (x e. B /\ xFy)) <-> E.x((x e. A /\ -. x e. B) /\ xFy))
40	27, 39	sylib 173	. . . . . 6 |- ((E.x(x e. A /\ xFy) /\ -. E.x(x e. B /\ xFy)) -> E.x((x e. A /\ -. x e. B) /\ xFy))
41	40	a1i 7	. . . . 5 |- (Fun `'F -> ((E.x(x e. A /\ xFy) /\ -. E.x(x e. B /\ xFy)) -> E.x((x e. A /\ -. x e. B) /\ xFy)))
42	25, 41	impbid 397	. . . 4 |- (Fun `'F -> (E.x((x e. A /\ -. x e. B) /\ xFy) <-> (E.x(x e. A /\ xFy) /\ -. E.x(x e. B /\ xFy))))
43		eldif 1496	. . . . . 6 |- (x e. (A \ B) <-> (x e. A /\ -. x e. B))
44	43	anbi1i 368	. . . . 5 |- ((x e. (A \ B) /\ xFy) <-> ((x e. A /\ -. x e. B) /\ xFy))
45	44	biex 733	. . . 4 |- (E.x(x e. (A \ B) /\ xFy) <-> E.x((x e. A /\ -. x e. B) /\ xFy))
46	6	elima2 2607	. . . . 5 |- (y e. (F"A) <-> E.x(x e. A /\ xFy))
47	6	elima2 2607	. . . . . 6 |- (y e. (F"B) <-> E.x(x e. B /\ xFy))
48	47	negbii 162	. . . . 5 |- (-. y e. (F"B) <-> -. E.x(x e. B /\ xFy))
49	46, 48	anbi12i 369	. . . 4 |- ((y e. (F"A) /\ -. y e. (F"B)) <-> (E.x(x e. A /\ xFy) /\ -. E.x(x e. B /\ xFy)))
50	42, 45, 49	3bitr4g 428	. . 3 |- (Fun `'F -> (E.x(x e. (A \ B) /\ xFy) <-> (y e. (F"A) /\ -. y e. (F"B))))
51	6	elima2 2607	. . 3 |- (y e. (F"(A \ B)) <-> E.x(x e. (A \ B) /\ xFy))
52		eldif 1496	. . 3 |- (y e. ((F"A) \ (F"B)) <-> (y e. (F"A) /\ -. y e. (F"B)))
53	50, 51, 52	3bitr4g 428	. 2 |- (Fun `'F -> (y e. (F"(A \ B)) <-> y e. ((F"A) \ (F"B))))
54	53	cleqrd 1100	1 |- (Fun `'F -> (F"(A \ B)) = ((F"A) \ (F"B)))

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195   /\ wa 196  A.wal 672  E.wex 678  E*wmo 1008   = wceq 1091   e. wcel 1092   \ cdif 1484   class class class wbr 2054  `'ccnv 2409  "cima 2413  Fun wfun 2416

This theorem is referenced by:  phplem5 3407  php3 3411

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432

metamath.org