Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imaundi | Structured version Visualization version GIF version |
Description: Distributive law for image over union. Theorem 35 of [Suppes] p. 65. (Contributed by NM, 30-Sep-2002.) |
Ref | Expression |
---|---|
imaundi | ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resundi 5862 | . . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) | |
2 | 1 | rneqi 5802 | . . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) |
3 | rnun 5999 | . . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) | |
4 | 2, 3 | eqtri 2844 | . 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) |
5 | df-ima 5563 | . 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶)) | |
6 | df-ima 5563 | . . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) | |
7 | df-ima 5563 | . . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
8 | 6, 7 | uneq12i 4137 | . 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) |
9 | 4, 5, 8 | 3eqtr4i 2854 | 1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∪ cun 3934 ran crn 5551 ↾ cres 5552 “ cima 5553 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4562 df-pr 4564 df-op 4568 df-br 5060 df-opab 5122 df-xp 5556 df-cnv 5558 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 |
This theorem is referenced by: fnimapr 6742 domunfican 8785 fiint 8789 fodomfi 8791 marypha1lem 8891 resunimafz0 13797 dprd2da 19158 dmdprdsplit2lem 19161 uniioombllem3 24180 mbfimaicc 24226 plyeq0 24795 fnimatp 30417 ffsrn 30459 tocyccntz 30781 noetalem4 33215 imadifss 34861 poimirlem1 34887 poimirlem2 34888 poimirlem3 34889 poimirlem4 34890 poimirlem6 34892 poimirlem7 34893 poimirlem11 34897 poimirlem12 34898 poimirlem15 34901 poimirlem16 34902 poimirlem17 34903 poimirlem19 34905 poimirlem20 34906 poimirlem23 34909 poimirlem24 34910 poimirlem25 34911 poimirlem29 34915 poimirlem31 34917 mbfposadd 34933 itg2addnclem2 34938 ftc1anclem1 34961 ftc1anclem5 34965 brtrclfv2 40065 frege77d 40084 frege109d 40095 frege131d 40102 dffrege76 40278 icccncfext 42162 |
Copyright terms: Public domain | W3C validator |