Theorem fvssunirn 6905

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

This proof depends on syntax axioms:   ⊆ wss 3899  ∪ cuni 4867  ran crn 5649  ‘cfv 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5656  df-dm 5658  df-rn 5659  df-iota 6484  df-fv 6536

This theorem is used by:  ovssunirn  7445  marypha2lem1  9405  acnlem  10084  fin23lem29  10376  itunitc  10456  hsmexlem5  10465  wunfv  10774  wunex2  10780  strfvss  17312  prdsvallem  17572  prdsval  17573  prdsbas  17575  prdsplusg  17576  prdsmulr  17577  prdsvsca  17578  prdshom  17585  mreunirn  17718  mrcfval  17729  mrcssv  17735  mrisval  17751  sscpwex  17937  wunfunc  18023  catcxpccl  18328  comppfsc  23798  filunirn  24148  elflim  24237  flffval  24255  fclsval  24274  isfcls  24275  fcfval  24299  tsmsxplem1  24419  xmetunirn  24603  mopnval  24704  tmsval  24747  cfilfval  25532  caufval  25543  issgon  34674  elrnsiga  34677  volmeas  34783  omssubadd  34852  neibastop2lem  37064  ctbssinf  38243  ismtyval  38648  dicval  42147  prjcrv0  43577  ismrc  43644  nacsfix  43655  hbt  44069