![]() |
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 5995 | . . . 4 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) | |
2 | 1 | rneqi 5936 | . . 3 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) |
3 | rnun 6145 | . . 3 ⊢ ran ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) | |
4 | 2, 3 | eqtri 2760 | . 2 ⊢ ran (𝐴 ↾ (𝐵 ∪ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) |
5 | df-ima 5689 | . 2 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ran (𝐴 ↾ (𝐵 ∪ 𝐶)) | |
6 | df-ima 5689 | . . 3 ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) | |
7 | df-ima 5689 | . . 3 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶) | |
8 | 6, 7 | uneq12i 4161 | . 2 ⊢ ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) = (ran (𝐴 ↾ 𝐵) ∪ ran (𝐴 ↾ 𝐶)) |
9 | 4, 5, 8 | 3eqtr4i 2770 | 1 ⊢ (𝐴 “ (𝐵 ∪ 𝐶)) = ((𝐴 “ 𝐵) ∪ (𝐴 “ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∪ cun 3946 ran crn 5677 ↾ cres 5678 “ cima 5679 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 df-opab 5211 df-xp 5682 df-cnv 5684 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 |
This theorem is referenced by: cnvimassrndm 6151 fnimapr 6975 naddasslem1 8692 naddasslem2 8693 imafi 9174 domunfican 9319 fiint 9323 fodomfi 9324 marypha1lem 9427 resunimafz0 14403 dprd2da 19911 dmdprdsplit2lem 19914 uniioombllem3 25101 mbfimaicc 25147 plyeq0 25724 madeoldsuc 27376 negsbdaylem 27527 fnimatp 31897 ffsrn 31949 tocyccntz 32298 imadifss 36458 poimirlem1 36484 poimirlem2 36485 poimirlem3 36486 poimirlem4 36487 poimirlem6 36489 poimirlem7 36490 poimirlem11 36494 poimirlem12 36495 poimirlem15 36498 poimirlem16 36499 poimirlem17 36500 poimirlem19 36502 poimirlem20 36503 poimirlem23 36506 poimirlem24 36507 poimirlem25 36508 poimirlem29 36512 poimirlem31 36514 mbfposadd 36530 itg2addnclem2 36535 ftc1anclem1 36556 ftc1anclem5 36560 brtrclfv2 42468 frege77d 42487 frege109d 42498 frege131d 42505 dffrege76 42680 icccncfext 44593 |
Copyright terms: Public domain | W3C validator |