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 6513

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 6512	. . 3 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))))
2		imadif 6512	. . . 4 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
3	2	difeq2d 4058	. . 3 ⊢ (Fun ^◡𝐹 → ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
4	1, 3	eqtrd 2778	. 2 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
5		dfin4 4203	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
6	5	imaeq2i 5962	. 2 ⊢ (𝐹 “ (𝐴 ∩ 𝐵)) = (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵)))
7		dfin4 4203	. 2 ⊢ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
8	4, 6, 7	3eqtr4g 2803	1 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1539 ∖ cdif 3885 ∩ cin 3887 ^◡ccnv 5585 “ cima 5589 Fun wfun 6422

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3433 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4259 df-if 4462 df-sn 4564 df-pr 4566 df-op 4570 df-br 5076 df-opab 5138 df-id 5486 df-xp 5592 df-rel 5593 df-cnv 5594 df-co 5595 df-dm 5596 df-rn 5597 df-res 5598 df-ima 5599 df-fun 6430

This theorem is referenced by: inpreima 6935 rnelfmlem 23092 fmfnfmlem3 23096 spthispth 28081 swrdrndisj 31216 ballotlemfrc 32480 poimirlem1 35765 poimirlem2 35766 poimirlem3 35767 poimirlem4 35768 poimirlem6 35770 poimirlem7 35771 poimirlem11 35775 poimirlem12 35776 poimirlem16 35780 poimirlem17 35781 poimirlem19 35783 poimirlem20 35784 poimirlem23 35787 poimirlem24 35788 poimirlem25 35789 poimirlem29 35793 poimirlem31 35795