Theorem imadif 6635

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 675	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
2	1	exbii 1843	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
3		19.40 1882	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
4	2, 3	sylbi 216	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
5		nfv 1910	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Fun ◡𝐹
6		nfe1 2140	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)
7	5, 6	nfan 1895	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵))
8		funmo 6566	. . . . . . . . . . . . . 14 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑦◡𝐹𝑥)
9		vex 3466	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
10		vex 3466	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
11	9, 10	brcnv 5881	. . . . . . . . . . . . . . 15 ⊢ (𝑦◡𝐹𝑥 ↔ 𝑥𝐹𝑦)
12	11	mobii 2537	. . . . . . . . . . . . . 14 ⊢ (∃*𝑥 𝑦◡𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
13	8, 12	sylib 217	. . . . . . . . . . . . 13 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14		mopick 2614	. . . . . . . . . . . . 13 ⊢ ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
15	13, 14	sylan 578	. . . . . . . . . . . 12 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
16	15	con2d 134	. . . . . . . . . . 11 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦))
17		imnan 398	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
18	16, 17	sylib 217	. . . . . . . . . 10 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
19	7, 18	alrimi 2202	. . . . . . . . 9 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
20	19	ex 411	. . . . . . . 8 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
21		exancom 1857	. . . . . . . 8 ⊢ (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
22		alnex 1776	. . . . . . . 8 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
23	20, 21, 22	3imtr3g 294	. . . . . . 7 ⊢ (Fun ◡𝐹 → (∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
24	23	anim2d 610	. . . . . 6 ⊢ (Fun ◡𝐹 → ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
25	4, 24	syl5 34	. . . . 5 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
26		19.29r 1870	. . . . . . 7 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
27	22, 26	sylan2br 593	. . . . . 6 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
28		andi 1005	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29		ianor 979	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦))
30	29	anbi2i 621	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31		an32 644	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵))
32		pm3.24 401	. . . . . . . . . . . 12 ⊢ ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
33	32	intnan 485	. . . . . . . . . . 11 ⊢ ¬ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34		anass 467	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
35	33, 34	mtbir 322	. . . . . . . . . 10 ⊢ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
36	35	biorfi 936	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
37	31, 36	bitri 274	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
38	28, 30, 37	3bitr4i 302	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
39	38	exbii 1843	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
40	27, 39	sylib 217	. . . . 5 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
41	25, 40	impbid1 224	. . . 4 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
42		eldif 3956	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
43	42	anbi1i 622	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
44	43	exbii 1843	. . . 4 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
45	9	elima2 6067	. . . . 5 ⊢ (𝑦 ∈ (𝐹 “ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))
46	9	elima2 6067	. . . . . 6 ⊢ (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
47	46	notbii 319	. . . . 5 ⊢ (¬ 𝑦 ∈ (𝐹 “ 𝐵) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
48	45, 47	anbi12i 626	. . . 4 ⊢ ((𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
49	41, 44, 48	3bitr4g 313	. . 3 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵))))
50	9	elima2 6067	. . 3 ⊢ (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦))
51		eldif 3956	. . 3 ⊢ (𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)))
52	49, 50, 51	3bitr4g 313	. 2 ⊢ (Fun ◡𝐹 → (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ 𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
53	52	eqrdv 2724	1 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∨ wo 845  ∀wal 1532   = wceq 1534  ∃wex 1774   ∈ wcel 2099  ∃*wmo 2527   ∖ cdif 3943   class class class wbr 5145  ^◡ccnv 5673   “ cima 5677  Fun wfun 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5146  df-opab 5208  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-fun 6548

This theorem is referenced by:  imain  6636  resdif  6856  difpreima  7070  domunsncan  9102  phplem2  9235  php3  9239  phplem4OLD  9247  php3OLD  9251  infdifsn  9693  cantnfp1lem3  9716  enfin1ai  10418  fin1a2lem7  10440  symgfixelsi  19429  dprdf1o  20028  frlmlbs  21791  f1lindf  21816  cnclima  23260  iscncl  23261  qtopcld  23705  qtoprest  23709  qtopcmap  23711  mbfimaicc  25648  ismbf3d  25671  i1fd  25698  ballotlemfrc  34373  poimirlem2  37336  poimirlem4  37338  poimirlem6  37340  poimirlem7  37341  poimirlem9  37343  poimirlem11  37345  poimirlem12  37346  poimirlem13  37347  poimirlem14  37348  poimirlem16  37350  poimirlem19  37353  poimirlem23  37357