Theorem fvssunirn 6853

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

Syntax hints:   ⊆ wss 3897  ∪ cuni 4856  ran crn 5615  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-cnv 5622  df-dm 5624  df-rn 5625  df-iota 6437  df-fv 6489

This theorem is referenced by:  ovssunirn  7382  marypha2lem1  9319  acnlem  9939  fin23lem29  10232  itunitc  10312  hsmexlem5  10321  wunfv  10623  wunex2  10629  strfvss  17098  prdsvallem  17358  prdsval  17359  prdsbas  17361  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  mreunirn  17503  mrcfval  17514  mrcssv  17520  mrisval  17536  sscpwex  17722  wunfunc  17808  catcxpccl  18113  comppfsc  23447  filunirn  23797  elflim  23886  flffval  23904  fclsval  23923  isfcls  23924  fcfval  23948  tsmsxplem1  24068  xmetunirn  24252  mopnval  24353  tmsval  24396  cfilfval  25191  caufval  25202  issgon  34136  elrnsiga  34139  volmeas  34244  omssubadd  34313  neibastop2lem  36404  ctbssinf  37450  ismtyval  37839  dicval  41274  prjcrv0  42725  ismrc  42793  nacsfix  42804  hbt  43222