Theorem fvssunirn 6938

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

Syntax hints:   ⊆ wss 3950  ∪ cuni 4906  ran crn 5685  ‘cfv 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-cnv 5692  df-dm 5694  df-rn 5695  df-iota 6513  df-fv 6568

This theorem is referenced by:  ovssunirn  7468  marypha2lem1  9476  acnlem  10089  fin23lem29  10382  itunitc  10462  hsmexlem5  10471  wunfv  10773  wunex2  10779  strfvss  17225  prdsvallem  17500  prdsval  17501  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  mreunirn  17645  mrcfval  17652  mrcssv  17658  mrisval  17674  sscpwex  17860  wunfunc  17947  catcxpccl  18253  comppfsc  23541  filunirn  23891  elflim  23980  flffval  23998  fclsval  24017  isfcls  24018  fcfval  24042  tsmsxplem1  24162  xmetunirn  24348  mopnval  24449  tmsval  24494  cfilfval  25299  caufval  25310  issgon  34125  elrnsiga  34128  volmeas  34233  omssubadd  34303  neibastop2lem  36362  ctbssinf  37408  ismtyval  37808  dicval  41179  prjcrv0  42648  ismrc  42717  nacsfix  42728  hbt  43147