Theorem fvssunirn 6913

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

This proof depends on syntax axioms:   ⊆ wss 3902  ∪ cuni 4870  ran crn 5660  ‘cfv 6537

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-cnv 5667  df-dm 5669  df-rn 5670  df-iota 6493  df-fv 6545

This theorem is used by:  ovssunirn  7452  marypha2lem1  9408  acnlem  10054  fin23lem29  10346  itunitc  10426  hsmexlem5  10435  wunfv  10744  wunex2  10750  strfvss  17283  prdsvallem  17543  prdsval  17544  prdsbas  17546  prdsplusg  17547  prdsmulr  17548  prdsvsca  17549  prdshom  17556  mreunirn  17689  mrcfval  17700  mrcssv  17706  mrisval  17722  sscpwex  17908  wunfunc  17994  catcxpccl  18299  comppfsc  23759  filunirn  24109  elflim  24198  flffval  24216  fclsval  24235  isfcls  24236  fcfval  24260  tsmsxplem1  24380  xmetunirn  24564  mopnval  24665  tmsval  24708  cfilfval  25493  caufval  25504  issgon  34620  elrnsiga  34623  volmeas  34729  omssubadd  34798  neibastop2lem  36966  ctbssinf  38147  ismtyval  38537  dicval  42036  prjcrv0  43466  ismrc  43533  nacsfix  43544  hbt  43958