Theorem fvssunirn 6936

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

This proof depends on syntax axioms:   ⊆ wss 3900  ∪ cuni 4870  ran crn 5656  ‘cfv 6555

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-cnv 5663  df-dm 5665  df-rn 5666  df-iota 6509  df-fv 6563

This theorem is used by:  ovssunirn  7476  marypha2lem1  9451  acnlem  10151  fin23lem29  10443  itunitc  10523  hsmexlem5  10532  wunfv  10841  wunex2  10847  strfvss  17391  prdsvallem  17651  prdsval  17652  prdsbas  17654  prdsplusg  17655  prdsmulr  17656  prdsvsca  17657  prdshom  17664  mreunirn  17797  mrcfval  17808  mrcssv  17814  mrisval  17830  sscpwex  18016  wunfunc  18102  catcxpccl  18407  comppfsc  23878  filunirn  24228  elflim  24317  flffval  24335  fclsval  24354  isfcls  24355  fcfval  24379  tsmsxplem1  24499  xmetunirn  24683  mopnval  24784  tmsval  24827  cfilfval  25612  caufval  25623  issgon  34822  elrnsiga  34825  volmeas  34931  omssubadd  34999  neibastop2lem  37325  ctbssinf  38520  ismtyval  38925  dicval  42424  prjcrv0  43860  ismrc  43903  nacsfix  43914  hbt  44322