imain - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > imain		Structured version Visualization version GIF version

Theorem imain 6618

Description: The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.)

**Assertion**
Ref	Expression
imain	⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))

**Proof of Theorem imain**
Step	Hyp	Ref	Expression
1		imadif 6617	. . 3 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))))
2		imadif 6617	. . . 4 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
3	2	difeq2d 4074	. . 3 ⊢ (Fun ^◡𝐹 → ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
4	1, 3	eqtrd 2795	. 2 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
5		dfin4 4224	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
6	5	imaeq2i 6054	. 2 ⊢ (𝐹 “ (𝐴 ∩ 𝐵)) = (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵)))
7		dfin4 4224	. 2 ⊢ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
8	4, 6, 7	3eqtr4g 2820	1 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∖ cdif 3896 ∩ cin 3898 ^◡ccnv 5654 “ cima 5658 Fun wfun 6527

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 2213 ax-ext 2732 ax-sep 5251 ax-pr 5398

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 2564 df-clab 2739 df-cleq 2752 df-clel 2835 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5168 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-fun 6535

This theorem is used by: inpreima 7056 rnelfmlem 24178 fmfnfmlem3 24182 spthispth 30188 swrdrndisj 33397 ballotlemfrc 35038 poimirlem1 38370 poimirlem2 38371 poimirlem3 38372 poimirlem4 38373 poimirlem6 38375 poimirlem7 38376 poimirlem11 38380 poimirlem12 38381 poimirlem16 38385 poimirlem17 38386 poimirlem19 38388 poimirlem20 38389 poimirlem23 38392 poimirlem24 38393 poimirlem25 38394 poimirlem29 38398 poimirlem31 38400