Theorem imadif 6570

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 677	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
2	1	exbii 1849	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
3		19.40 1887	. . . . . . 7 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
4	2, 3	sylbi 217	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
5		nfv 1915	. . . . . . . . . . 11 ⊢ Ⅎ𝑥Fun ◡𝐹
6		nfe1 2155	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)
7	5, 6	nfan 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑥(Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵))
8		funmo 6502	. . . . . . . . . . . . . 14 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑦◡𝐹𝑥)
9		vex 3441	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
10		vex 3441	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
11	9, 10	brcnv 5826	. . . . . . . . . . . . . . 15 ⊢ (𝑦◡𝐹𝑥 ↔ 𝑥𝐹𝑦)
12	11	mobii 2545	. . . . . . . . . . . . . 14 ⊢ (∃*𝑥 𝑦◡𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦)
13	8, 12	sylib 218	. . . . . . . . . . . . 13 ⊢ (Fun ◡𝐹 → ∃*𝑥 𝑥𝐹𝑦)
14		mopick 2622	. . . . . . . . . . . . 13 ⊢ ((∃*𝑥 𝑥𝐹𝑦 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
15	13, 14	sylan 580	. . . . . . . . . . . 12 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥𝐹𝑦 → ¬ 𝑥 ∈ 𝐵))
16	15	con2d 134	. . . . . . . . . . 11 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → (𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦))
17		imnan 399	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 → ¬ 𝑥𝐹𝑦) ↔ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
18	16, 17	sylib 218	. . . . . . . . . 10 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
19	7, 18	alrimi 2218	. . . . . . . . 9 ⊢ ((Fun ◡𝐹 ∧ ∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵)) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
20	19	ex 412	. . . . . . . 8 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) → ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
21		exancom 1862	. . . . . . . 8 ⊢ (∃𝑥(𝑥𝐹𝑦 ∧ ¬ 𝑥 ∈ 𝐵) ↔ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
22		alnex 1782	. . . . . . . 8 ⊢ (∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
23	20, 21, 22	3imtr3g 295	. . . . . . 7 ⊢ (Fun ◡𝐹 → (∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) → ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
24	23	anim2d 612	. . . . . 6 ⊢ (Fun ◡𝐹 → ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∃𝑥(¬ 𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
25	4, 24	syl5 34	. . . . 5 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
26		19.29r 1875	. . . . . . 7 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ∀𝑥 ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
27	22, 26	sylan2br 595	. . . . . 6 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
28		andi 1009	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
29		ianor 983	. . . . . . . . 9 ⊢ (¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦) ↔ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦))
30	29	anbi2i 623	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ (¬ 𝑥 ∈ 𝐵 ∨ ¬ 𝑥𝐹𝑦)))
31		an32 646	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵))
32		pm3.24 402	. . . . . . . . . . . 12 ⊢ ¬ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)
33	32	intnan 486	. . . . . . . . . . 11 ⊢ ¬ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦))
34		anass 468	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝑥𝐹𝑦 ∧ ¬ 𝑥𝐹𝑦)))
35	33, 34	mtbir 323	. . . . . . . . . 10 ⊢ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)
36	35	biorfri 939	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
37	31, 36	bitri 275	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥 ∈ 𝐵) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ 𝑥𝐹𝑦)))
38	28, 30, 37	3bitr4i 303	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
39	38	exbii 1849	. . . . . 6 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ (𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
40	27, 39	sylib 218	. . . . 5 ⊢ ((∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)) → ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
41	25, 40	impbid1 225	. . . 4 ⊢ (Fun ◡𝐹 → (∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))))
42		eldif 3908	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
43	42	anbi1i 624	. . . . 5 ⊢ ((𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
44	43	exbii 1849	. . . 4 ⊢ (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ ∃𝑥((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵) ∧ 𝑥𝐹𝑦))
45	9	elima2 6019	. . . . 5 ⊢ (𝑦 ∈ (𝐹 “ 𝐴) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))
46	9	elima2 6019	. . . . . 6 ⊢ (𝑦 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
47	46	notbii 320	. . . . 5 ⊢ (¬ 𝑦 ∈ (𝐹 “ 𝐵) ↔ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦))
48	45, 47	anbi12i 628	. . . 4 ⊢ ((𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ∧ ¬ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥𝐹𝑦)))
49	41, 44, 48	3bitr4g 314	. . 3 ⊢ (Fun ◡𝐹 → (∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵))))
50	9	elima2 6019	. . 3 ⊢ (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ ∃𝑥(𝑥 ∈ (𝐴 ∖ 𝐵) ∧ 𝑥𝐹𝑦))
51		eldif 3908	. . 3 ⊢ (𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ↔ (𝑦 ∈ (𝐹 “ 𝐴) ∧ ¬ 𝑦 ∈ (𝐹 “ 𝐵)))
52	49, 50, 51	3bitr4g 314	. 2 ⊢ (Fun ◡𝐹 → (𝑦 ∈ (𝐹 “ (𝐴 ∖ 𝐵)) ↔ 𝑦 ∈ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
53	52	eqrdv 2731	1 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∃*wmo 2535   ∖ cdif 3895   class class class wbr 5093  ^◡ccnv 5618   “ cima 5622  Fun wfun 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6488

This theorem is referenced by:  imain  6571  f1imadifssran  6572  resdif  6789  difpreima  7004  domunsncan  8997  phplem2  9121  php3  9125  infdifsn  9554  cantnfp1lem3  9577  enfin1ai  10282  fin1a2lem7  10304  symgfixelsi  19349  dprdf1o  19948  frlmlbs  21736  f1lindf  21761  cnclima  23184  iscncl  23185  qtopcld  23629  qtoprest  23633  qtopcmap  23635  mbfimaicc  25560  ismbf3d  25583  i1fd  25610  ballotlemfrc  34561  poimirlem2  37683  poimirlem4  37685  poimirlem6  37687  poimirlem7  37688  poimirlem9  37690  poimirlem11  37692  poimirlem12  37693  poimirlem13  37694  poimirlem14  37695  poimirlem16  37697  poimirlem19  37700  poimirlem23  37704