Theorem fvssunirn 6933

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

Syntax hints:   ⊆ wss 3947  ∪ cuni 4910  ran crn 5681  ‘cfv 6551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-opab 5213  df-cnv 5688  df-dm 5690  df-rn 5691  df-iota 6503  df-fv 6559

This theorem is referenced by:  ovssunirn  7460  marypha2lem1  9464  acnlem  10077  fin23lem29  10370  itunitc  10450  hsmexlem5  10459  wunfv  10761  wunex2  10767  strfvss  17161  prdsvallem  17441  prdsval  17442  prdsbas  17444  prdsplusg  17445  prdsmulr  17446  prdsvsca  17447  prdshom  17454  mreunirn  17586  mrcfval  17593  mrcssv  17599  mrisval  17615  sscpwex  17803  wunfunc  17892  wunfuncOLD  17893  catcxpccl  18203  catcxpcclOLD  18204  comppfsc  23454  filunirn  23804  elflim  23893  flffval  23911  fclsval  23930  isfcls  23931  fcfval  23955  tsmsxplem1  24075  xmetunirn  24261  mopnval  24362  tmsval  24407  cfilfval  25210  caufval  25221  issgon  33747  elrnsiga  33750  volmeas  33855  omssubadd  33925  neibastop2lem  35849  ctbssinf  36890  ismtyval  37278  dicval  40653  prjcrv0  42060  ismrc  42124  nacsfix  42135  hbt  42557