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 6639

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 6638	. . 3 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))))
2		imadif 6638	. . . 4 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
3	2	difeq2d 4118	. . 3 ⊢ (Fun ^◡𝐹 → ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
4	1, 3	eqtrd 2765	. 2 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
5		dfin4 4266	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
6	5	imaeq2i 6062	. 2 ⊢ (𝐹 “ (𝐴 ∩ 𝐵)) = (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵)))
7		dfin4 4266	. 2 ⊢ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
8	4, 6, 7	3eqtr4g 2790	1 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1533 ∖ cdif 3941 ∩ cin 3943 ^◡ccnv 5677 “ cima 5681 Fun wfun 6543

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-fun 6551

This theorem is referenced by: inpreima 7072 rnelfmlem 23905 fmfnfmlem3 23909 spthispth 29617 swrdrndisj 32772 ballotlemfrc 34279 poimirlem1 37227 poimirlem2 37228 poimirlem3 37229 poimirlem4 37230 poimirlem6 37232 poimirlem7 37233 poimirlem11 37237 poimirlem12 37238 poimirlem16 37242 poimirlem17 37243 poimirlem19 37245 poimirlem20 37246 poimirlem23 37249 poimirlem24 37250 poimirlem25 37251 poimirlem29 37255 poimirlem31 37257