![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvssunirn | Structured version Visualization version GIF version |
Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by SN, 13-Jan-2025.) |
Ref | Expression |
---|---|
fvssunirn | ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfvunirn 6932 | . 2 ⊢ (𝑥 ∈ (𝐹‘𝑋) → 𝑥 ∈ ∪ ran 𝐹) | |
2 | 1 | ssriv 3984 | 1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: ⊆ wss 3947 ∪ cuni 4910 ran crn 5681 ‘cfv 6551 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-ne 2937 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-opab 5213 df-cnv 5688 df-dm 5690 df-rn 5691 df-iota 6503 df-fv 6559 |
This theorem is referenced by: ovssunirn 7460 marypha2lem1 9464 acnlem 10077 fin23lem29 10370 itunitc 10450 hsmexlem5 10459 wunfv 10761 wunex2 10767 strfvss 17161 prdsvallem 17441 prdsval 17442 prdsbas 17444 prdsplusg 17445 prdsmulr 17446 prdsvsca 17447 prdshom 17454 mreunirn 17586 mrcfval 17593 mrcssv 17599 mrisval 17615 sscpwex 17803 wunfunc 17892 wunfuncOLD 17893 catcxpccl 18203 catcxpcclOLD 18204 comppfsc 23454 filunirn 23804 elflim 23893 flffval 23911 fclsval 23930 isfcls 23931 fcfval 23955 tsmsxplem1 24075 xmetunirn 24261 mopnval 24362 tmsval 24407 cfilfval 25210 caufval 25221 issgon 33747 elrnsiga 33750 volmeas 33855 omssubadd 33925 neibastop2lem 35849 ctbssinf 36890 ismtyval 37278 dicval 40653 prjcrv0 42060 ismrc 42124 nacsfix 42135 hbt 42557 |
Copyright terms: Public domain | W3C validator |