Theorem imadif 6584

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

Assertion

Ref	Expression
imadif	⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))

Proof of Theorem imadif

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		anandir 678	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
2	1	exbii 1850	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
3		19.40 1888	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
4	2, 3	sylbi 217	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
5		nfv 1916	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Fun ◡𝐹
6		nfe1 2156	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)
7	5, 6	nfan 1901	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵))
8		funmo 6516	. . . . . . . . . . . . . 14 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑦◡𝐹𝑥)
9		vex 3446	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
10		vex 3446	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
11	9, 10	brcnv 5839	. . . . . . . . . . . . . . 15 ⊢ (𝑦◡𝐹𝑥 ↔ 𝑥𝐹𝑦)
12	11	mobii 2549	. . . . . . . . . . . . . 14 ⊢ (∃*𝑥 𝑦◡𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
13	8, 12	sylib 218	. . . . . . . . . . . . 13 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14		mopick 2626	. . . . . . . . . . . . 13 ⊢ ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
15	13, 14	sylan 581	. . . . . . . . . . . 12 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
16	15	con2d 134	. . . . . . . . . . 11 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦))
17		imnan 399	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
18	16, 17	sylib 218	. . . . . . . . . 10 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
19	7, 18	alrimi 2221	. . . . . . . . 9 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
20	19	ex 412	. . . . . . . 8 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
21		exancom 1863	. . . . . . . 8 ⊢ (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
22		alnex 1783	. . . . . . . 8 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
23	20, 21, 22	3imtr3g 295	. . . . . . 7 ⊢ (Fun ◡𝐹 → (∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
24	23	anim2d 613	. . . . . 6 ⊢ (Fun ◡𝐹 → ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
25	4, 24	syl5 34	. . . . 5 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
26		19.29r 1876	. . . . . . 7 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
27	22, 26	sylan2br 596	. . . . . 6 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
28		andi 1010	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29		ianor 984	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦))
30	29	anbi2i 624	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31		an32 647	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵))
32		pm3.24 402	. . . . . . . . . . . 12 ⊢ ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
33	32	intnan 486	. . . . . . . . . . 11 ⊢ ¬ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34		anass 468	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
35	33, 34	mtbir 323	. . . . . . . . . 10 ⊢ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
36	35	biorfri 940	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
37	31, 36	bitri 275	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
38	28, 30, 37	3bitr4i 303	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
39	38	exbii 1850	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
40	27, 39	sylib 218	. . . . 5 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
41	25, 40	impbid1 225	. . . 4 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
42		eldif 3913	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
43	42	anbi1i 625	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
44	43	exbii 1850	. . . 4 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
45	9	elima2 6033	. . . . 5 ⊢ (𝑦 ∈ (𝐹 “ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))
46	9	elima2 6033	. . . . . 6 ⊢ (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
47	46	notbii 320	. . . . 5 ⊢ (¬ 𝑦 ∈ (𝐹 “ 𝐵) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
48	45, 47	anbi12i 629	. . . 4 ⊢ ((𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
49	41, 44, 48	3bitr4g 314	. . 3 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵))))
50	9	elima2 6033	. . 3 ⊢ (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦))
51		eldif 3913	. . 3 ⊢ (𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)))
52	49, 50, 51	3bitr4g 314	. 2 ⊢ (Fun ◡𝐹 → (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ 𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
53	52	eqrdv 2735	1 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃*wmo 2538   ∖ cdif 3900   class class class wbr 5100  ^◡ccnv 5631   “ cima 5635  Fun wfun 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502

This theorem is referenced by:  imain  6585  f1imadifssran  6586  resdif  6803  difpreima  7019  domunsncan  9017  phplem2  9141  php3  9145  infdifsn  9578  cantnfp1lem3  9601  enfin1ai  10306  fin1a2lem7  10328  symgfixelsi  19376  dprdf1o  19975  frlmlbs  21764  f1lindf  21789  cnclima  23224  iscncl  23225  qtopcld  23669  qtoprest  23673  qtopcmap  23675  mbfimaicc  25600  ismbf3d  25623  i1fd  25650  ballotlemfrc  34704  poimirlem2  37867  poimirlem4  37869  poimirlem6  37871  poimirlem7  37872  poimirlem9  37874  poimirlem11  37876  poimirlem12  37877  poimirlem13  37878  poimirlem14  37879  poimirlem16  37881  poimirlem19  37884  poimirlem23  37888