MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvssunirn Structured version   Visualization version   GIF version

Theorem fvssunirn 6871
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.)
Assertion
Ref Expression
fvssunirn (𝐹𝑋) ⊆ ran 𝐹

Proof of Theorem fvssunirn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elfvunirn 6870 . 2 (𝑥 ∈ (𝐹𝑋) → 𝑥 ran 𝐹)
21ssriv 3947 1 (𝐹𝑋) ⊆ ran 𝐹
Colors of variables: wff setvar class
Syntax hints:  wss 3909   cuni 4864  ran crn 5632  cfv 6492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2943  df-ral 3064  df-rex 3073  df-rab 3407  df-v 3446  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-cnv 5639  df-dm 5641  df-rn 5642  df-iota 6444  df-fv 6500
This theorem is referenced by:  ovssunirn  7386  marypha2lem1  9305  acnlem  9918  fin23lem29  10211  itunitc  10291  hsmexlem5  10300  wunfv  10602  wunex2  10608  strfvss  16994  prdsvallem  17271  prdsval  17272  prdsbas  17274  prdsplusg  17275  prdsmulr  17276  prdsvsca  17277  prdshom  17284  mreunirn  17416  mrcfval  17423  mrcssv  17429  mrisval  17445  sscpwex  17633  wunfunc  17720  wunfuncOLD  17721  catcxpccl  18030  catcxpcclOLD  18031  comppfsc  22806  filunirn  23156  elflim  23245  flffval  23263  fclsval  23282  isfcls  23283  fcfval  23307  tsmsxplem1  23427  xmetunirn  23613  mopnval  23714  tmsval  23759  cfilfval  24551  caufval  24562  issgon  32496  elrnsiga  32499  volmeas  32604  omssubadd  32674  neibastop2lem  34728  ctbssinf  35773  ismtyval  36155  dicval  39535  prjcrv0  40837  ismrc  40890  nacsfix  40901  hbt  41323
  Copyright terms: Public domain W3C validator