Theorem fnfvelrn 7025

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ran crn 5625   Fn wfn 6487  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  ffvelcdm  7026  fnfvelrnd  7027  fvcofneq  7038  fnovrn  7533  offvalfv  7644  fo1stres  7959  fo2ndres  7960  offsplitfpar  8061  fo2ndf  8063  seqomlem3  8383  seqomlem4  8384  phplem2  9129  indexfi  9260  dffi3  9334  ordtypelem7  9429  inf0  9530  infdifsn  9566  noinfep  9569  cantnflem3  9600  cantnf  9602  cardinfima  10007  alephfplem1  10014  alephfplem3  10016  alephfp  10018  dfac5  10039  dfac12lem2  10055  cfflb  10169  sornom  10187  fin23lem16  10245  fin23lem20  10247  isf32lem2  10264  axcc2lem  10346  axdc3lem2  10361  ttukeylem6  10424  konigthlem  10479  pwcfsdom  10494  pwfseqlem1  10569  gch2  10586  1nn  12156  peano2nn  12157  rpnnen1lem5  12894  om2uzrani  13875  uzrdglem  13880  uzrdg0i  13882  fseqsupubi  13901  ccatrn  14513  uzin2  15268  climsup  15593  ruclem12  16166  0ram  16948  setcepi  18012  acsmapd  18477  cycsubgcl  19135  ghmrn  19158  conjnmz  19181  pmtrrn  19386  sylow1lem4  19530  pgpssslw  19543  sylow2blem3  19551  sylow3lem2  19557  efgsfo  19668  gexex  19782  gsumval3eu  19833  gsumzsplit  19856  pjfo  21670  issubassa2  21848  mplbas2  21997  mpfconst  22064  mpfproj  22065  mpfind  22070  pf1const  22290  pf1id  22291  mpfpf1  22295  pf1mpf  22296  toprntopon  22869  cmpsub  23344  conncn  23370  2ndcctbss  23399  2ndcdisj  23400  2ndcsep  23403  iskgen2  23492  kgen2cn  23503  ptbasfi  23525  ptcnplem  23565  isr0  23681  r0cld  23682  zfbas  23840  uzrest  23841  rnelfm  23897  tmdgsum2  24040  evth  24914  bcth3  25287  ivthicc  25415  ovolmge0  25434  ovollb2lem  25445  ovolunlem1a  25453  ovoliunlem1  25459  ovoliun  25462  ovolicc2lem4  25477  voliunlem1  25507  voliunlem3  25509  volsup  25513  ioombl1lem2  25516  ioombl1lem4  25518  uniioombllem2  25540  uniioombllem3  25542  vitalilem2  25566  vitalilem4  25568  mbflimsup  25623  itg11  25648  i1faddlem  25650  i1fmullem  25651  itg1mulc  25661  i1fres  25662  itg1climres  25671  mbfi1fseqlem3  25674  itg2seq  25699  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  itg2cnlem1  25718  limciun  25851  dvcnvlem  25936  dvivthlem2  25970  dvivth  25971  lhop1lem  25974  lhop1  25975  lhop2  25976  aalioulem3  26298  basellem3  27049  nodenselem8  27659  noseq0  28286  noseqp1  28287  noseqrdg0  28303  tgelrnln  28702  wlkiswwlks1  29940  ubthlem1  30945  pjrni  31777  pjoi0  31792  hmopidmchi  32226  hmopidmpji  32227  pjssdif1i  32250  dfpjop  32257  pjadj3  32263  elpjrn  32265  pjcmul1i  32276  pjcmul2i  32277  pj3si  32282  ofrn2  32718  prodindf  32944  mgcf1o  33085  cycpmfvlem  33194  cycpmfv1  33195  cycpmfv2  33196  locfinreflem  33997  cnre2csqlem  34067  elmrsubrn  35714  elmsubrn  35722  msubrn  35723  elmsta  35742  vhmcls  35760  mclsppslem  35777  neibastop2lem  36554  tailfb  36571  fvineqsneu  37616  ptrecube  37821  heicant  37856  mblfinlem2  37859  ftc1anclem7  37900  ftc1anc  37902  sstotbnd2  37975  prdsbnd  37994  heibor1lem  38010  heiborlem1  38012  dihcl  41530  dih0rn  41544  dih1dimatlem  41589  dihlspsnssN  41592  dochocss  41626  hdmaprnlem17N  42123  hgmaprnlem1N  42156  nacsfix  42954  kercvrlsm  43325  pwssplit4  43331  tfsconcatrev  43590  orbitinit  45197  orbitcl  45198  climinf  45852  climinf2lem  45950  limsupvaluz2  45982  supcnvlimsup  45984  fourierdlem25  46376  fourierdlem42  46393  fourierdlem54  46404  fourierdlem64  46414  fourierdlem65  46415  sge0le  46651  sge0seq  46690  imaelsetpreimafv  47641