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 3939	1 ⊢ (𝐹‘𝑋) ⊆ ∪ ran 𝐹

Syntax hints:   ⊆ wss 3903  ∪ cuni 4858  ran crn 5620  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630  df-iota 6438  df-fv 6490

This theorem is referenced by:  ovssunirn  7385  marypha2lem1  9325  acnlem  9942  fin23lem29  10235  itunitc  10315  hsmexlem5  10324  wunfv  10626  wunex2  10632  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  23417  filunirn  23767  elflim  23856  flffval  23874  fclsval  23893  isfcls  23894  fcfval  23918  tsmsxplem1  24038  xmetunirn  24223  mopnval  24324  tmsval  24367  cfilfval  25162  caufval  25173  issgon  34106  elrnsiga  34109  volmeas  34214  omssubadd  34284  neibastop2lem  36354  ctbssinf  37400  ismtyval  37800  dicval  41175  prjcrv0  42626  ismrc  42694  nacsfix  42705  hbt  43123