Theorem imadif 6621

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 690	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
2	1	exbii 1881	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
3		19.40 1919	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
4	2, 3	sylbi 220	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
5		nfv 1947	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Fun ◡𝐹
6		nfe1 2187	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)
7	5, 6	nfan 1932	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵))
8		funmo 6553	. . . . . . . . . . . . . 14 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑦◡𝐹𝑥)
9		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
10		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
11	9, 10	brcnv 5866	. . . . . . . . . . . . . . 15 ⊢ (𝑦◡𝐹𝑥 ↔ 𝑥𝐹𝑦)
12	11	mobii 2575	. . . . . . . . . . . . . 14 ⊢ (∃*𝑥 𝑦◡𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
13	8, 12	sylib 221	. . . . . . . . . . . . 13 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14		mopick 2652	. . . . . . . . . . . . 13 ⊢ ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
15	13, 14	sylan 592	. . . . . . . . . . . 12 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
16	15	con2d 135	. . . . . . . . . . 11 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦))
17		imnan 405	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
18	16, 17	sylib 221	. . . . . . . . . 10 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
19	7, 18	alrimi 2251	. . . . . . . . 9 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
20	19	ex 418	. . . . . . . 8 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
21		exancom 1894	. . . . . . . 8 ⊢ (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
22		alnex 1814	. . . . . . . 8 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
23	20, 21, 22	3imtr3g 298	. . . . . . 7 ⊢ (Fun ◡𝐹 → (∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
24	23	anim2d 624	. . . . . 6 ⊢ (Fun ◡𝐹 → ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
25	4, 24	syl5 35	. . . . 5 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
26		19.29r 1907	. . . . . . 7 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
27	22, 26	sylan2br 607	. . . . . 6 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
28		andi 1025	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29		ianor 997	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦))
30	29	anbi2i 635	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31		an32 659	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵))
32		pm3.24 408	. . . . . . . . . . . 12 ⊢ ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
33	32	intnan 492	. . . . . . . . . . 11 ⊢ ¬ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34		anass 474	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
35	33, 34	mtbir 326	. . . . . . . . . 10 ⊢ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
36	35	biorfri 953	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
37	31, 36	bitri 278	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
38	28, 30, 37	3bitr4i 306	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
39	38	exbii 1881	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
40	27, 39	sylib 221	. . . . 5 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
41	25, 40	impbid1 228	. . . 4 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
42		eldif 3912	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
43	42	anbi1i 636	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
44	43	exbii 1881	. . . 4 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
45	9	elima2 6066	. . . . 5 ⊢ (𝑦 ∈ (𝐹 “ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))
46	9	elima2 6066	. . . . . 6 ⊢ (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
47	46	notbii 323	. . . . 5 ⊢ (¬ 𝑦 ∈ (𝐹 “ 𝐵) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
48	45, 47	anbi12i 640	. . . 4 ⊢ ((𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
49	41, 44, 48	3bitr4g 317	. . 3 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵))))
50	9	elima2 6066	. . 3 ⊢ (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦))
51		eldif 3912	. . 3 ⊢ (𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)))
52	49, 50, 51	3bitr4g 317	. 2 ⊢ (Fun ◡𝐹 → (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ 𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
53	52	eqrdv 2760	1 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃*wmo 2564   ∖ cdif 3899   class class class wbr 5107  ^◡ccnv 5658   “ cima 5662  Fun wfun 6531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6539

This theorem is used by:  imain  6622  resdif  6843  difpreima  7061  domunsncan  9079  phplem2  9203  php3  9207  infdifsn  9640  cantnfp1lem3  9663  enfin1ai  10390  fin1a2lem7  10412  symgfixelsi  19568  dprdf1o  20167  frlmlbs  22016  f1lindf  22041  cnclima  23499  iscncl  23500  qtopcld  23945  qtoprest  23949  qtopcmap  23951  mbfimaicc  25865  ismbf3d  25888  i1fd  25915  ballotlemfrc  35046  poimirlem2  38379  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem9  38386  poimirlem11  38388  poimirlem12  38389  poimirlem13  38390  poimirlem14  38391  poimirlem16  38393  poimirlem19  38396  poimirlem23  38400