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 6625

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 6624	. . 3 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))))
2		imadif 6624	. . . 4 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
3	2	difeq2d 4081	. . 3 ⊢ (Fun ^◡𝐹 → ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
4	1, 3	eqtrd 2800	. 2 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))))
5		dfin4 4231	. . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵))
6	5	imaeq2i 6062	. 2 ⊢ (𝐹 “ (𝐴 ∩ 𝐵)) = (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵)))
7		dfin4 4231	. 2 ⊢ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))
8	4, 6, 7	3eqtr4g 2825	1 ⊢ (Fun ^◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∖ cdif 3903 ∩ cin 3905 ^◡ccnv 5662 “ cima 5666 Fun wfun 6534

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 2148 ax-9 2156 ax-10 2179 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-pr 5406

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 2569 df-clab 2744 df-cleq 2757 df-clel 2840 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-br 5112 df-opab 5176 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-fun 6542

This theorem is used by: inpreima 7063 rnelfmlem 24160 fmfnfmlem3 24164 spthispth 30136 swrdrndisj 33341 ballotlemfrc 34982 poimirlem1 38329 poimirlem2 38330 poimirlem3 38331 poimirlem4 38332 poimirlem6 38334 poimirlem7 38335 poimirlem11 38339 poimirlem12 38340 poimirlem16 38344 poimirlem17 38345 poimirlem19 38347 poimirlem20 38348 poimirlem23 38351 poimirlem24 38352 poimirlem25 38353 poimirlem29 38357 poimirlem31 38359