Theorem fnfvelrn 7021

Description: A function's value belongs to its range. (Contributed by NM, 15-Oct-1996.)

Assertion

Ref	Expression
fnfvelrn	⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹)

Proof of Theorem fnfvelrn

Step	Hyp	Ref	Expression
1		fvelrn 7017	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐹‘𝐵) ∈ ran 𝐹)
2	1	funfni 6591	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ran crn 5619   Fn wfn 6480  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-iota 6441  df-fun 6487  df-fn 6488  df-fv 6493

This theorem is referenced by:  ffvelcdm  7022  fnfvelrnd  7023  fvcofneq  7034  fnovrn  7531  offvalfv  7642  fo1stres  7957  fo2ndres  7958  offsplitfpar  8058  fo2ndf  8060  seqomlem3  8381  seqomlem4  8382  phplem2  9129  indexfi  9260  dffi3  9334  ordtypelem7  9429  inf0  9533  infdifsn  9569  noinfep  9572  cantnflem3  9603  cantnf  9605  cardinfima  10010  alephfplem1  10017  alephfplem3  10019  alephfp  10021  dfac5  10042  dfac12lem2  10058  cfflb  10172  sornom  10190  fin23lem16  10248  fin23lem20  10250  isf32lem2  10267  axcc2lem  10349  axdc3lem2  10364  ttukeylem6  10427  konigthlem  10482  pwcfsdom  10497  pwfseqlem1  10572  gch2  10589  1nn  12176  peano2nn  12177  rpnnen1lem5  12922  om2uzrani  13905  uzrdglem  13910  uzrdg0i  13912  fseqsupubi  13931  ccatrn  14543  uzin2  15298  climsup  15623  ruclem12  16199  0ram  16982  setcepi  18046  acsmapd  18511  cycsubgcl  19172  ghmrn  19195  conjnmz  19218  pmtrrn  19423  sylow1lem4  19567  pgpssslw  19580  sylow2blem3  19588  sylow3lem2  19594  efgsfo  19705  gexex  19819  gsumval3eu  19870  gsumzsplit  19893  pjfo  21690  issubassa2  21867  mplbas2  22018  mpfconst  22085  mpfproj  22086  mpfind  22091  pf1const  22332  pf1id  22333  mpfpf1  22337  pf1mpf  22338  toprntopon  22908  cmpsub  23383  conncn  23409  2ndcctbss  23438  2ndcdisj  23439  2ndcsep  23442  iskgen2  23531  kgen2cn  23542  ptbasfi  23564  ptcnplem  23604  isr0  23720  r0cld  23721  zfbas  23879  uzrest  23880  rnelfm  23936  tmdgsum2  24079  evth  24944  bcth3  25316  ivthicc  25443  ovolmge0  25462  ovollb2lem  25473  ovolunlem1a  25481  ovoliunlem1  25487  ovoliun  25490  ovolicc2lem4  25505  voliunlem1  25535  voliunlem3  25537  volsup  25541  ioombl1lem2  25544  ioombl1lem4  25546  uniioombllem2  25568  uniioombllem3  25570  vitalilem2  25594  vitalilem4  25596  mbflimsup  25651  itg11  25676  i1faddlem  25678  i1fmullem  25679  itg1mulc  25689  i1fres  25690  itg1climres  25699  mbfi1fseqlem3  25702  itg2seq  25727  itg2monolem2  25736  itg2monolem3  25737  itg2mono  25738  itg2cnlem1  25746  limciun  25879  dvcnvlem  25961  dvivthlem2  25994  dvivth  25995  lhop1lem  25998  lhop1  25999  lhop2  26000  aalioulem3  26318  basellem3  27064  nodenselem8  27673  noseq0  28300  noseqp1  28301  noseqrdg0  28317  tgelrnln  28716  wlkiswwlks1  29953  ubthlem1  30959  pjrni  31791  pjoi0  31806  hmopidmchi  32240  hmopidmpji  32241  pjssdif1i  32264  dfpjop  32271  pjadj3  32277  elpjrn  32279  pjcmul1i  32290  pjcmul2i  32291  pj3si  32296  ofrn2  32732  prodindf  32941  mgcf1o  33082  cycpmfvlem  33193  cycpmfv1  33194  cycpmfv2  33195  locfinreflem  34024  cnre2csqlem  34094  elmrsubrn  35748  elmsubrn  35756  msubrn  35757  elmsta  35776  vhmcls  35794  mclsppslem  35811  neibastop2lem  36588  tailfb  36605  fvineqsneu  37773  ptrecube  37987  heicant  38022  mblfinlem2  38025  ftc1anclem7  38066  ftc1anc  38068  sstotbnd2  38141  prdsbnd  38160  heibor1lem  38176  heiborlem1  38178  dihcl  41762  dih0rn  41776  dih1dimatlem  41821  dihlspsnssN  41824  dochocss  41858  hdmaprnlem17N  42355  hgmaprnlem1N  42388  nacsfix  43161  kercvrlsm  43528  pwssplit4  43534  tfsconcatrev  43793  orbitinit  45400  orbitcl  45401  climinf  46051  climinf2lem  46149  limsupvaluz2  46181  supcnvlimsup  46183  fourierdlem25  46575  fourierdlem42  46592  fourierdlem54  46603  fourierdlem64  46613  fourierdlem65  46614  sge0le  46850  sge0seq  46889  imaelsetpreimafv  47870