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 6570

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 6569	. . 3 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))))
2		imadif 6569	. . . 4 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
3	2	difeq2d 4057	. . 3 ⊢ (Fun ^◡𝐹 → ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
4	1, 3	eqtrd 2774	. 2 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
5		dfin4 4206	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
6	5	imaeq2i 6010	. 2 ⊢ (𝐹 “ (𝐴 ∩ 𝐵)) = (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵)))
7		dfin4 4206	. 2 ⊢ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
8	4, 6, 7	3eqtr4g 2799	1 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1547 ∖ cdif 3880 ∩ cin 3882 ^◡ccnv 5617 “ cima 5621 Fun wfun 6479

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-pr 5362

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-clab 2718 df-cleq 2731 df-clel 2814 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-sn 4556 df-pr 4558 df-op 4562 df-br 5073 df-opab 5135 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-fun 6487

This theorem is referenced by: inpreima 7005 rnelfmlem 23935 fmfnfmlem3 23939 spthispth 29810 swrdrndisj 33036 ballotlemfrc 34711 poimirlem1 37988 poimirlem2 37989 poimirlem3 37990 poimirlem4 37991 poimirlem6 37993 poimirlem7 37994 poimirlem11 37998 poimirlem12 37999 poimirlem16 38003 poimirlem17 38004 poimirlem19 38006 poimirlem20 38007 poimirlem23 38010 poimirlem24 38011 poimirlem25 38012 poimirlem29 38016 poimirlem31 38018