Theorem fnfvelrn 7073

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 7069	. 2 ⊢ ((Fun 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐹‘𝐵) ∈ ran 𝐹)
2	1	funfni 6639	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹‘𝐵) ∈ ran 𝐹)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ran crn 5660   Fn wfn 6529  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6490  df-fun 6536  df-fn 6537  df-fv 6542

This theorem is referenced by:  ffvelcdm  7074  fnfvelrnd  7075  fvcofneq  7086  fnovrn  7583  offvalfv  7694  fo1stres  8008  fo2ndres  8009  offsplitfpar  8110  fo2ndf  8112  seqomlem3  8435  seqomlem4  8436  phplem2  9185  indexfi  9313  dffi3  9387  ordtypelem7  9482  inf0  9586  infdifsn  9622  noinfep  9625  cantnflem3  9656  cantnf  9658  cardinfima  10077  alephfplem1  10084  alephfplem3  10086  alephfp  10088  dfac5  10108  dfac12lem2  10124  cfflb  10239  sornom  10257  fin23lem16  10315  fin23lem20  10317  isf32lem2  10334  axcc2lem  10416  axdc3lem2  10431  ttukeylem6  10494  konigthlem  10549  pwcfsdom  10564  pwfseqlem1  10639  gch2  10656  1nn  12240  peano2nn  12241  rpnnen1lem5  13001  om2uzrani  13984  uzrdglem  13989  uzrdg0i  13991  fseqsupubi  14010  ccatrn  14623  sgnrn  15131  uzin2  15392  climsup  15717  ruclem12  16293  0ram  17076  setcepi  18141  acsmapd  18606  cycsubgcl  19273  ghmrn  19295  conjnmz  19318  pmtrrn  19523  sylow1lem4  19667  pgpssslw  19680  sylow2blem3  19688  sylow3lem2  19694  efgsfo  19805  gexex  19919  gsumval3eu  19970  gsumzsplit  19993  pjfo  21830  issubassa2  22007  mplbas2  22158  mpfconst  22225  mpfproj  22226  mpfind  22231  pf1const  22471  pf1id  22472  mpfpf1  22476  pf1mpf  22477  toprntopon  23047  cmpsub  23522  conncn  23548  2ndcctbss  23577  2ndcdisj  23578  2ndcsep  23581  iskgen2  23670  kgen2cn  23681  ptbasfi  23703  ptcnplem  23743  isr0  23859  r0cld  23860  zfbas  24018  uzrest  24019  rnelfm  24075  tmdgsum2  24218  evth  25083  bcth3  25455  ivthicc  25582  ovolmge0  25601  ovollb2lem  25612  ovolunlem1a  25620  ovoliunlem1  25626  ovoliun  25629  ovolicc2lem4  25644  voliunlem1  25674  voliunlem3  25676  volsup  25680  ioombl1lem2  25683  ioombl1lem4  25685  uniioombllem2  25707  uniioombllem3  25709  vitalilem2  25733  vitalilem4  25735  mbflimsup  25790  itg11  25815  i1faddlem  25817  i1fmullem  25818  itg1mulc  25828  i1fres  25829  itg1climres  25838  mbfi1fseqlem3  25841  itg2seq  25866  itg2monolem2  25875  itg2monolem3  25876  itg2mono  25877  itg2cnlem1  25885  limciun  26018  dvcnvlem  26100  dvivthlem2  26133  dvivth  26134  lhop1lem  26137  lhop1  26138  lhop2  26139  aalioulem3  26460  basellem3  27209  nodenselem8  27817  noseq0  28445  noseqp1  28446  noseqrdg0  28462  tgelrnln  28861  wlkiswwlks1  30153  ubthlem1  31159  pjrni  31991  pjoi0  32006  hmopidmchi  32440  hmopidmpji  32441  pjssdif1i  32464  dfpjop  32471  pjadj3  32477  elpjrn  32479  pjcmul1i  32490  pjcmul2i  32491  pj3si  32496  ofrn2  32922  prodindf  33119  mgcf1o  33260  cycpmfvlem  33369  cycpmfv1  33370  cycpmfv2  33371  locfinreflem  34171  cnre2csqlem  34241  elmrsubrn  35907  elmsubrn  35915  msubrn  35916  elmsta  35935  vhmcls  35953  mclsppslem  35970  neibastop2lem  36756  tailfb  36773  fvineqsneu  37940  ptrecube  38154  heicant  38189  mblfinlem2  38192  ftc1anclem7  38233  ftc1anc  38235  sstotbnd2  38308  prdsbnd  38327  heibor1lem  38343  heiborlem1  38345  dihcl  41929  dih0rn  41943  dih1dimatlem  41988  dihlspsnssN  41991  dochocss  42025  hdmaprnlem17N  42522  hgmaprnlem1N  42555  nacsfix  43330  kercvrlsm  43697  pwssplit4  43703  tfsconcatrev  43962  orbitinit  45552  orbitcl  45553  climinf  46209  climinf2lem  46307  limsupvaluz2  46339  supcnvlimsup  46341  fourierdlem25  46733  fourierdlem42  46750  fourierdlem54  46761  fourierdlem64  46771  fourierdlem65  46772  sge0le  47008  sge0seq  47047  imaelsetpreimafv  48028