Theorem fnfvelrn 7090

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ran crn 5679   Fn wfn 6543  ‘cfv 6548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-iota 6500  df-fun 6550  df-fn 6551  df-fv 6556

This theorem is referenced by:  ffvelcdm  7091  fnfvelrnd  7092  fvcofneq  7103  fnovrn  7596  fo1stres  8019  fo2ndres  8020  offsplitfpar  8124  fo2ndf  8126  seqomlem3  8472  seqomlem4  8473  phplem2  9232  phplem4OLD  9244  indexfi  9384  dffi3  9454  ordtypelem7  9547  inf0  9644  infdifsn  9680  noinfep  9683  cantnflem3  9714  cantnf  9716  cardinfima  10120  alephfplem1  10127  alephfplem3  10129  alephfp  10131  dfac5  10151  dfac12lem2  10167  cfflb  10282  sornom  10300  fin23lem16  10358  fin23lem20  10360  isf32lem2  10377  axcc2lem  10459  axdc3lem2  10474  ttukeylem6  10537  konigthlem  10591  pwcfsdom  10606  pwfseqlem1  10681  gch2  10698  1nn  12253  peano2nn  12254  rpnnen1lem5  12995  om2uzrani  13949  uzrdglem  13954  uzrdg0i  13956  fseqsupubi  13975  ccatrn  14571  uzin2  15323  climsup  15648  ruclem12  16217  0ram  16988  setcepi  18076  acsmapd  18545  cycsubgcl  19160  ghmrn  19182  conjnmz  19205  pmtrrn  19411  sylow1lem4  19555  pgpssslw  19568  sylow2blem3  19576  sylow3lem2  19582  efgsfo  19693  gexex  19807  gsumval3eu  19858  gsumzsplit  19881  pjfo  21648  issubassa2  21824  mplbas2  21979  mpfconst  22046  mpfproj  22047  mpfind  22052  pf1const  22264  pf1id  22265  mpfpf1  22269  pf1mpf  22270  toprntopon  22826  cmpsub  23303  conncn  23329  2ndcctbss  23358  2ndcdisj  23359  2ndcsep  23362  iskgen2  23451  kgen2cn  23462  ptbasfi  23484  ptcnplem  23524  isr0  23640  r0cld  23641  zfbas  23799  uzrest  23800  rnelfm  23856  tmdgsum2  23999  evth  24884  bcth3  25258  ivthicc  25386  ovolmge0  25405  ovollb2lem  25416  ovolunlem1a  25424  ovoliunlem1  25430  ovoliun  25433  ovolicc2lem4  25448  voliunlem1  25478  voliunlem3  25480  volsup  25484  ioombl1lem2  25487  ioombl1lem4  25489  uniioombllem2  25511  uniioombllem3  25513  vitalilem2  25537  vitalilem4  25539  mbflimsup  25594  itg11  25619  i1faddlem  25621  i1fmullem  25622  itg1mulc  25633  i1fres  25634  itg1climres  25643  mbfi1fseqlem3  25646  itg2seq  25671  itg2monolem2  25680  itg2monolem3  25681  itg2mono  25682  itg2cnlem1  25690  limciun  25822  dvcnvlem  25907  dvivthlem2  25941  dvivth  25942  lhop1lem  25945  lhop1  25946  lhop2  25947  aalioulem3  26268  basellem3  27014  nodenselem8  27623  noseq0  28162  noseqp1  28163  noseqrdg0  28179  tgelrnln  28433  wlkiswwlks1  29677  ubthlem1  30679  pjrni  31511  pjoi0  31526  hmopidmchi  31960  hmopidmpji  31961  pjssdif1i  31984  dfpjop  31991  pjadj3  31997  elpjrn  31999  pjcmul1i  32010  pjcmul2i  32011  pj3si  32016  ofrn2  32425  mgcf1o  32730  cycpmfvlem  32833  cycpmfv1  32834  cycpmfv2  32835  locfinreflem  33441  cnre2csqlem  33511  prodindf  33642  elmrsubrn  35130  elmsubrn  35138  msubrn  35139  elmsta  35158  vhmcls  35176  mclsppslem  35193  neibastop2lem  35844  tailfb  35861  fvineqsneu  36890  ptrecube  37093  heicant  37128  mblfinlem2  37131  ftc1anclem7  37172  ftc1anc  37174  sstotbnd2  37247  prdsbnd  37266  heibor1lem  37282  heiborlem1  37284  dihcl  40743  dih0rn  40757  dih1dimatlem  40802  dihlspsnssN  40805  dochocss  40839  hdmaprnlem17N  41336  hgmaprnlem1N  41369  nacsfix  42132  kercvrlsm  42507  pwssplit4  42513  tfsconcatrev  42777  ssmapsn  44589  climinf  44994  climinf2lem  45094  limsupvaluz2  45126  supcnvlimsup  45128  fourierdlem25  45520  fourierdlem42  45537  fourierdlem54  45548  fourierdlem64  45558  fourierdlem65  45559  sge0le  45795  sge0seq  45834  imaelsetpreimafv  46735  offvalfv  47406