Theorem fvssunirn 6866

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.

Step	Hyp	Ref	Expression
1		elfvunirn 6865	. 2 ⊢ (𝑥 ∈ (𝐹‘𝑋) → 𝑥 ∈ ∪ ran 𝐹)
2	1	ssriv 3938	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ⊆ wss 3902  ∪ cuni 4864  ran crn 5626  ‘cfv 6493

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-cnv 5633  df-dm 5635  df-rn 5636  df-iota 6449  df-fv 6501

This theorem is referenced by:  ovssunirn  7396  marypha2lem1  9342  acnlem  9962  fin23lem29  10255  itunitc  10335  hsmexlem5  10344  wunfv  10647  wunex2  10653  strfvss  17118  prdsvallem  17378  prdsval  17379  prdsbas  17381  prdsplusg  17382  prdsmulr  17383  prdsvsca  17384  prdshom  17391  mreunirn  17524  mrcfval  17535  mrcssv  17541  mrisval  17557  sscpwex  17743  wunfunc  17829  catcxpccl  18134  comppfsc  23480  filunirn  23830  elflim  23919  flffval  23937  fclsval  23956  isfcls  23957  fcfval  23981  tsmsxplem1  24101  xmetunirn  24285  mopnval  24386  tmsval  24429  cfilfval  25224  caufval  25235  issgon  34282  elrnsiga  34285  volmeas  34390  omssubadd  34459  neibastop2lem  36556  ctbssinf  37613  ismtyval  38003  dicval  41504  prjcrv0  42943  ismrc  43010  nacsfix  43021  hbt  43439