Theorem fvssunirn 6916

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

Syntax hints:   ⊆ wss 3913  ∪ cuni 4877  ran crn 5666  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-12 2220  ax-ext 2742  ax-sep 5262  ax-nul 5274  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-ne 2966  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-cnv 5673  df-dm 5675  df-rn 5676  df-iota 6496  df-fv 6548

This theorem is referenced by:  ovssunirn  7450  marypha2lem1  9398  acnlem  10035  fin23lem29  10328  itunitc  10408  hsmexlem5  10417  wunfv  10720  wunex2  10726  strfvss  17250  prdsvallem  17510  prdsval  17511  prdsbas  17513  prdsplusg  17514  prdsmulr  17515  prdsvsca  17516  prdshom  17523  mreunirn  17656  mrcfval  17667  mrcssv  17673  mrisval  17689  sscpwex  17875  wunfunc  17961  catcxpccl  18266  comppfsc  23672  filunirn  24022  elflim  24111  flffval  24129  fclsval  24148  isfcls  24149  fcfval  24173  tsmsxplem1  24293  xmetunirn  24477  mopnval  24578  tmsval  24621  cfilfval  25406  caufval  25417  issgon  34483  elrnsiga  34486  volmeas  34591  omssubadd  34660  neibastop2lem  36819  ctbssinf  38000  ismtyval  38399  dicval  41900  prjcrv0  43317  ismrc  43384  nacsfix  43395  hbt  43809