Theorem fvssunirn 6875

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

Syntax hints:   ⊆ wss 3903  ∪ cuni 4865  ran crn 5635  ‘cfv 6502

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 5245  ax-nul 5255  ax-pr 5381

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5642  df-dm 5644  df-rn 5645  df-iota 6458  df-fv 6510

This theorem is referenced by:  ovssunirn  7406  marypha2lem1  9352  acnlem  9972  fin23lem29  10265  itunitc  10345  hsmexlem5  10354  wunfv  10657  wunex2  10663  strfvss  17128  prdsvallem  17388  prdsval  17389  prdsbas  17391  prdsplusg  17392  prdsmulr  17393  prdsvsca  17394  prdshom  17401  mreunirn  17534  mrcfval  17545  mrcssv  17551  mrisval  17567  sscpwex  17753  wunfunc  17839  catcxpccl  18144  comppfsc  23493  filunirn  23843  elflim  23932  flffval  23950  fclsval  23969  isfcls  23970  fcfval  23994  tsmsxplem1  24114  xmetunirn  24298  mopnval  24399  tmsval  24442  cfilfval  25237  caufval  25248  issgon  34307  elrnsiga  34310  volmeas  34415  omssubadd  34484  neibastop2lem  36582  ctbssinf  37688  ismtyval  38080  dicval  41581  prjcrv0  43020  ismrc  43087  nacsfix  43098  hbt  43516