Theorem fvssunirn 6862

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 6861	. 2 ⊢ (𝑥 ∈ (𝐹‘𝑋) → 𝑥 ∈ ∪ ran 𝐹)
2	1	ssriv 3921	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ⊆ wss 3885  ∪ cuni 4841  ran crn 5622  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-cnv 5629  df-dm 5631  df-rn 5632  df-iota 6445  df-fv 6497

This theorem is referenced by:  ovssunirn  7396  marypha2lem1  9342  acnlem  9965  fin23lem29  10258  itunitc  10338  hsmexlem5  10347  wunfv  10650  wunex2  10656  strfvss  17152  prdsvallem  17412  prdsval  17413  prdsbas  17415  prdsplusg  17416  prdsmulr  17417  prdsvsca  17418  prdshom  17425  mreunirn  17558  mrcfval  17569  mrcssv  17575  mrisval  17591  sscpwex  17777  wunfunc  17863  catcxpccl  18168  comppfsc  23519  filunirn  23869  elflim  23958  flffval  23976  fclsval  23995  isfcls  23996  fcfval  24020  tsmsxplem1  24140  xmetunirn  24324  mopnval  24425  tmsval  24468  cfilfval  25253  caufval  25264  issgon  34319  elrnsiga  34322  volmeas  34427  omssubadd  34496  neibastop2lem  36603  ctbssinf  37783  ismtyval  38182  dicval  41683  prjcrv0  43098  ismrc  43165  nacsfix  43176  hbt  43590