![]() |
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 5445 | . . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) | |
2 | 1 | rneqi 5384 | . . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) |
3 | rnun 5576 | . . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) | |
4 | 2, 3 | eqtri 2673 | . 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) |
5 | df-ima 5156 | . 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶)) | |
6 | df-ima 5156 | . . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) | |
7 | df-ima 5156 | . . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
8 | 6, 7 | uneq12i 3798 | . 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) |
9 | 4, 5, 8 | 3eqtr4i 2683 | 1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ∪ cun 3605 ran crn 5144 ↾ cres 5145 “ cima 5146 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-xp 5149 df-cnv 5151 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 |
This theorem is referenced by: fnimapr 6301 domunfican 8274 fiint 8278 fodomfi 8280 marypha1lem 8380 resunimafz0 13267 dprd2da 18487 dmdprdsplit2lem 18490 uniioombllem3 23399 mbfimaicc 23445 plyeq0 24012 ffsrn 29632 noetalem4 31991 imadifss 33514 poimirlem1 33540 poimirlem2 33541 poimirlem3 33542 poimirlem4 33543 poimirlem6 33545 poimirlem7 33546 poimirlem11 33550 poimirlem12 33551 poimirlem15 33554 poimirlem16 33555 poimirlem17 33556 poimirlem19 33558 poimirlem20 33559 poimirlem23 33562 poimirlem24 33563 poimirlem25 33564 poimirlem29 33568 poimirlem31 33570 mbfposadd 33587 itg2addnclem2 33592 ftc1anclem1 33615 ftc1anclem5 33619 brtrclfv2 38336 frege77d 38355 frege109d 38366 frege131d 38373 dffrege76 38550 icccncfext 40418 |
Copyright terms: Public domain | W3C validator |