![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imain | Structured version Visualization version GIF version |
Description: The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009.) |
Ref | Expression |
---|---|
imain | ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imadif 6185 | . . 3 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵)))) | |
2 | imadif 6185 | . . . 4 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ 𝐵)) = ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))) | |
3 | 2 | difeq2d 3927 | . . 3 ⊢ (Fun ◡𝐹 → ((𝐹 “ 𝐴) ∖ (𝐹 “ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))) |
4 | 1, 3 | eqtrd 2834 | . 2 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)))) |
5 | dfin4 4069 | . . 3 ⊢ (𝐴 ∩ 𝐵) = (𝐴 ∖ (𝐴 ∖ 𝐵)) | |
6 | 5 | imaeq2i 5682 | . 2 ⊢ (𝐹 “ (𝐴 ∩ 𝐵)) = (𝐹 “ (𝐴 ∖ (𝐴 ∖ 𝐵))) |
7 | dfin4 4069 | . 2 ⊢ ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵)) = ((𝐹 “ 𝐴) ∖ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵))) | |
8 | 4, 6, 7 | 3eqtr4g 2859 | 1 ⊢ (Fun ◡𝐹 → (𝐹 “ (𝐴 ∩ 𝐵)) = ((𝐹 “ 𝐴) ∩ (𝐹 “ 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∖ cdif 3767 ∩ cin 3769 ◡ccnv 5312 “ cima 5316 Fun wfun 6096 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2378 ax-ext 2778 ax-sep 4976 ax-nul 4984 ax-pr 5098 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2592 df-eu 2610 df-clab 2787 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3388 df-dif 3773 df-un 3775 df-in 3777 df-ss 3784 df-nul 4117 df-if 4279 df-sn 4370 df-pr 4372 df-op 4376 df-br 4845 df-opab 4907 df-id 5221 df-xp 5319 df-rel 5320 df-cnv 5321 df-co 5322 df-dm 5323 df-rn 5324 df-res 5325 df-ima 5326 df-fun 6104 |
This theorem is referenced by: inpreima 6569 rnelfmlem 22083 fmfnfmlem3 22087 spthispth 26979 ballotlemfrc 31104 poimirlem1 33898 poimirlem2 33899 poimirlem3 33900 poimirlem4 33901 poimirlem6 33903 poimirlem7 33904 poimirlem11 33908 poimirlem12 33909 poimirlem16 33913 poimirlem17 33914 poimirlem19 33916 poimirlem20 33917 poimirlem23 33920 poimirlem24 33921 poimirlem25 33922 poimirlem29 33926 poimirlem31 33928 |
Copyright terms: Public domain | W3C validator |