Theorem fvssunirn 6864

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

Syntax hints:   ⊆ wss 3900  ∪ cuni 4862  ran crn 5624  ‘cfv 6491

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2932  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-cnv 5631  df-dm 5633  df-rn 5634  df-iota 6447  df-fv 6499

This theorem is referenced by:  ovssunirn  7394  marypha2lem1  9340  acnlem  9960  fin23lem29  10253  itunitc  10333  hsmexlem5  10342  wunfv  10645  wunex2  10651  strfvss  17116  prdsvallem  17376  prdsval  17377  prdsbas  17379  prdsplusg  17380  prdsmulr  17381  prdsvsca  17382  prdshom  17389  mreunirn  17522  mrcfval  17533  mrcssv  17539  mrisval  17555  sscpwex  17741  wunfunc  17827  catcxpccl  18132  comppfsc  23478  filunirn  23828  elflim  23917  flffval  23935  fclsval  23954  isfcls  23955  fcfval  23979  tsmsxplem1  24099  xmetunirn  24283  mopnval  24384  tmsval  24427  cfilfval  25222  caufval  25233  issgon  34259  elrnsiga  34262  volmeas  34367  omssubadd  34436  neibastop2lem  36533  ctbssinf  37580  ismtyval  37970  dicval  41471  prjcrv0  42913  ismrc  42980  nacsfix  42991  hbt  43409