Theorem fnfvelrn 7099

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ran crn 5689   Fn wfn 6557  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-fv 6570

This theorem is referenced by:  ffvelcdm  7100  fnfvelrnd  7101  fvcofneq  7112  fnovrn  7607  offvalfv  7718  fo1stres  8038  fo2ndres  8039  offsplitfpar  8142  fo2ndf  8144  seqomlem3  8490  seqomlem4  8491  phplem2  9242  phplem4OLD  9254  indexfi  9397  dffi3  9468  ordtypelem7  9561  inf0  9658  infdifsn  9694  noinfep  9697  cantnflem3  9728  cantnf  9730  cardinfima  10134  alephfplem1  10141  alephfplem3  10143  alephfp  10145  dfac5  10166  dfac12lem2  10182  cfflb  10296  sornom  10314  fin23lem16  10372  fin23lem20  10374  isf32lem2  10391  axcc2lem  10473  axdc3lem2  10488  ttukeylem6  10551  konigthlem  10605  pwcfsdom  10620  pwfseqlem1  10695  gch2  10712  1nn  12274  peano2nn  12275  rpnnen1lem5  13020  om2uzrani  13989  uzrdglem  13994  uzrdg0i  13996  fseqsupubi  14015  ccatrn  14623  uzin2  15379  climsup  15702  ruclem12  16273  0ram  17053  setcepi  18141  acsmapd  18611  cycsubgcl  19236  ghmrn  19259  conjnmz  19282  pmtrrn  19489  sylow1lem4  19633  pgpssslw  19646  sylow2blem3  19654  sylow3lem2  19660  efgsfo  19771  gexex  19885  gsumval3eu  19936  gsumzsplit  19959  pjfo  21752  issubassa2  21929  mplbas2  22077  mpfconst  22142  mpfproj  22143  mpfind  22148  pf1const  22365  pf1id  22366  mpfpf1  22370  pf1mpf  22371  toprntopon  22946  cmpsub  23423  conncn  23449  2ndcctbss  23478  2ndcdisj  23479  2ndcsep  23482  iskgen2  23571  kgen2cn  23582  ptbasfi  23604  ptcnplem  23644  isr0  23760  r0cld  23761  zfbas  23919  uzrest  23920  rnelfm  23976  tmdgsum2  24119  evth  25004  bcth3  25378  ivthicc  25506  ovolmge0  25525  ovollb2lem  25536  ovolunlem1a  25544  ovoliunlem1  25550  ovoliun  25553  ovolicc2lem4  25568  voliunlem1  25598  voliunlem3  25600  volsup  25604  ioombl1lem2  25607  ioombl1lem4  25609  uniioombllem2  25631  uniioombllem3  25633  vitalilem2  25657  vitalilem4  25659  mbflimsup  25714  itg11  25739  i1faddlem  25741  i1fmullem  25742  itg1mulc  25753  i1fres  25754  itg1climres  25763  mbfi1fseqlem3  25766  itg2seq  25791  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2cnlem1  25810  limciun  25943  dvcnvlem  26028  dvivthlem2  26062  dvivth  26063  lhop1lem  26066  lhop1  26067  lhop2  26068  aalioulem3  26390  basellem3  27140  nodenselem8  27750  noseq0  28310  noseqp1  28311  noseqrdg0  28327  tgelrnln  28652  wlkiswwlks1  29896  ubthlem1  30898  pjrni  31730  pjoi0  31745  hmopidmchi  32179  hmopidmpji  32180  pjssdif1i  32203  dfpjop  32210  pjadj3  32216  elpjrn  32218  pjcmul1i  32229  pjcmul2i  32230  pj3si  32235  ofrn2  32656  mgcf1o  32977  cycpmfvlem  33114  cycpmfv1  33115  cycpmfv2  33116  locfinreflem  33800  cnre2csqlem  33870  prodindf  34003  elmrsubrn  35504  elmsubrn  35512  msubrn  35513  elmsta  35532  vhmcls  35550  mclsppslem  35567  neibastop2lem  36342  tailfb  36359  fvineqsneu  37393  ptrecube  37606  heicant  37641  mblfinlem2  37644  ftc1anclem7  37685  ftc1anc  37687  sstotbnd2  37760  prdsbnd  37779  heibor1lem  37795  heiborlem1  37797  dihcl  41252  dih0rn  41266  dih1dimatlem  41311  dihlspsnssN  41314  dochocss  41348  hdmaprnlem17N  41845  hgmaprnlem1N  41878  nacsfix  42699  kercvrlsm  43071  pwssplit4  43077  tfsconcatrev  43337  climinf  45561  climinf2lem  45661  limsupvaluz2  45693  supcnvlimsup  45695  fourierdlem25  46087  fourierdlem42  46104  fourierdlem54  46115  fourierdlem64  46125  fourierdlem65  46126  sge0le  46362  sge0seq  46401  imaelsetpreimafv  47319