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  16995  prdsvallem  17272  prdsval  17273  prdsbas  17275  prdsplusg  17276  prdsmulr  17277  prdsvsca  17278  prdshom  17285  mreunirn  17417  mrcfval  17424  mrcssv  17430  mrisval  17446  sscpwex  17634  wunfunc  17721  wunfuncOLD  17722  catcxpccl  18031  catcxpcclOLD  18032  comppfsc  22811  filunirn  23161  elflim  23250  flffval  23268  fclsval  23287  isfcls  23288  fcfval  23312  tsmsxplem1  23432  xmetunirn  23618  mopnval  23719  tmsval  23764  cfilfval  24556  caufval  24567  issgon  32502  elrnsiga  32505  volmeas  32610  omssubadd  32680  neibastop2lem  34763  ctbssinf  35808  ismtyval  36190  dicval  39570  prjcrv0  40873  ismrc  40926  nacsfix  40937  hbt  41359
  Copyright terms: Public domain W3C validator