Theorem fnfvelrn 7034

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ran crn 5633   Fn wfn 6495  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508

This theorem is referenced by:  ffvelcdm  7035  fnfvelrnd  7036  fvcofneq  7047  fnovrn  7543  offvalfv  7654  fo1stres  7969  fo2ndres  7970  offsplitfpar  8071  fo2ndf  8073  seqomlem3  8393  seqomlem4  8394  phplem2  9141  indexfi  9272  dffi3  9346  ordtypelem7  9441  inf0  9542  infdifsn  9578  noinfep  9581  cantnflem3  9612  cantnf  9614  cardinfima  10019  alephfplem1  10026  alephfplem3  10028  alephfp  10030  dfac5  10051  dfac12lem2  10067  cfflb  10181  sornom  10199  fin23lem16  10257  fin23lem20  10259  isf32lem2  10276  axcc2lem  10358  axdc3lem2  10373  ttukeylem6  10436  konigthlem  10491  pwcfsdom  10506  pwfseqlem1  10581  gch2  10598  1nn  12168  peano2nn  12169  rpnnen1lem5  12906  om2uzrani  13887  uzrdglem  13892  uzrdg0i  13894  fseqsupubi  13913  ccatrn  14525  uzin2  15280  climsup  15605  ruclem12  16178  0ram  16960  setcepi  18024  acsmapd  18489  cycsubgcl  19147  ghmrn  19170  conjnmz  19193  pmtrrn  19398  sylow1lem4  19542  pgpssslw  19555  sylow2blem3  19563  sylow3lem2  19569  efgsfo  19680  gexex  19794  gsumval3eu  19845  gsumzsplit  19868  pjfo  21682  issubassa2  21860  mplbas2  22009  mpfconst  22076  mpfproj  22077  mpfind  22082  pf1const  22302  pf1id  22303  mpfpf1  22307  pf1mpf  22308  toprntopon  22881  cmpsub  23356  conncn  23382  2ndcctbss  23411  2ndcdisj  23412  2ndcsep  23415  iskgen2  23504  kgen2cn  23515  ptbasfi  23537  ptcnplem  23577  isr0  23693  r0cld  23694  zfbas  23852  uzrest  23853  rnelfm  23909  tmdgsum2  24052  evth  24926  bcth3  25299  ivthicc  25427  ovolmge0  25446  ovollb2lem  25457  ovolunlem1a  25465  ovoliunlem1  25471  ovoliun  25474  ovolicc2lem4  25489  voliunlem1  25519  voliunlem3  25521  volsup  25525  ioombl1lem2  25528  ioombl1lem4  25530  uniioombllem2  25552  uniioombllem3  25554  vitalilem2  25578  vitalilem4  25580  mbflimsup  25635  itg11  25660  i1faddlem  25662  i1fmullem  25663  itg1mulc  25673  i1fres  25674  itg1climres  25683  mbfi1fseqlem3  25686  itg2seq  25711  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2cnlem1  25730  limciun  25863  dvcnvlem  25948  dvivthlem2  25982  dvivth  25983  lhop1lem  25986  lhop1  25987  lhop2  25988  aalioulem3  26310  basellem3  27061  nodenselem8  27671  noseq0  28298  noseqp1  28299  noseqrdg0  28315  tgelrnln  28714  wlkiswwlks1  29952  ubthlem1  30958  pjrni  31790  pjoi0  31805  hmopidmchi  32239  hmopidmpji  32240  pjssdif1i  32263  dfpjop  32270  pjadj3  32276  elpjrn  32278  pjcmul1i  32289  pjcmul2i  32290  pj3si  32295  ofrn2  32730  prodindf  32955  mgcf1o  33096  cycpmfvlem  33206  cycpmfv1  33207  cycpmfv2  33208  locfinreflem  34018  cnre2csqlem  34088  elmrsubrn  35736  elmsubrn  35744  msubrn  35745  elmsta  35764  vhmcls  35782  mclsppslem  35799  neibastop2lem  36576  tailfb  36593  fvineqsneu  37666  ptrecube  37871  heicant  37906  mblfinlem2  37909  ftc1anclem7  37950  ftc1anc  37952  sstotbnd2  38025  prdsbnd  38044  heibor1lem  38060  heiborlem1  38062  dihcl  41646  dih0rn  41660  dih1dimatlem  41705  dihlspsnssN  41708  dochocss  41742  hdmaprnlem17N  42239  hgmaprnlem1N  42272  nacsfix  43069  kercvrlsm  43440  pwssplit4  43446  tfsconcatrev  43705  orbitinit  45312  orbitcl  45313  climinf  45966  climinf2lem  46064  limsupvaluz2  46096  supcnvlimsup  46098  fourierdlem25  46490  fourierdlem42  46507  fourierdlem54  46518  fourierdlem64  46528  fourierdlem65  46529  sge0le  46765  sge0seq  46804  imaelsetpreimafv  47755