Theorem fnfvelrn 7008

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ran crn 5612   Fn wfn 6471  ‘cfv 6476

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 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-iota 6432  df-fun 6478  df-fn 6479  df-fv 6484

This theorem is referenced by:  ffvelcdm  7009  fnfvelrnd  7010  fvcofneq  7021  fnovrn  7516  offvalfv  7627  fo1stres  7942  fo2ndres  7943  offsplitfpar  8044  fo2ndf  8046  seqomlem3  8366  seqomlem4  8367  phplem2  9109  indexfi  9239  dffi3  9310  ordtypelem7  9405  inf0  9506  infdifsn  9542  noinfep  9545  cantnflem3  9576  cantnf  9578  cardinfima  9983  alephfplem1  9990  alephfplem3  9992  alephfp  9994  dfac5  10015  dfac12lem2  10031  cfflb  10145  sornom  10163  fin23lem16  10221  fin23lem20  10223  isf32lem2  10240  axcc2lem  10322  axdc3lem2  10337  ttukeylem6  10400  konigthlem  10454  pwcfsdom  10469  pwfseqlem1  10544  gch2  10561  1nn  12131  peano2nn  12132  rpnnen1lem5  12874  om2uzrani  13854  uzrdglem  13859  uzrdg0i  13861  fseqsupubi  13880  ccatrn  14492  uzin2  15247  climsup  15572  ruclem12  16145  0ram  16927  setcepi  17990  acsmapd  18455  cycsubgcl  19113  ghmrn  19136  conjnmz  19159  pmtrrn  19364  sylow1lem4  19508  pgpssslw  19521  sylow2blem3  19529  sylow3lem2  19535  efgsfo  19646  gexex  19760  gsumval3eu  19811  gsumzsplit  19834  pjfo  21647  issubassa2  21824  mplbas2  21972  mpfconst  22031  mpfproj  22032  mpfind  22037  pf1const  22256  pf1id  22257  mpfpf1  22261  pf1mpf  22262  toprntopon  22835  cmpsub  23310  conncn  23336  2ndcctbss  23365  2ndcdisj  23366  2ndcsep  23369  iskgen2  23458  kgen2cn  23469  ptbasfi  23491  ptcnplem  23531  isr0  23647  r0cld  23648  zfbas  23806  uzrest  23807  rnelfm  23863  tmdgsum2  24006  evth  24880  bcth3  25253  ivthicc  25381  ovolmge0  25400  ovollb2lem  25411  ovolunlem1a  25419  ovoliunlem1  25425  ovoliun  25428  ovolicc2lem4  25443  voliunlem1  25473  voliunlem3  25475  volsup  25479  ioombl1lem2  25482  ioombl1lem4  25484  uniioombllem2  25506  uniioombllem3  25508  vitalilem2  25532  vitalilem4  25534  mbflimsup  25589  itg11  25614  i1faddlem  25616  i1fmullem  25617  itg1mulc  25627  i1fres  25628  itg1climres  25637  mbfi1fseqlem3  25640  itg2seq  25665  itg2monolem2  25674  itg2monolem3  25675  itg2mono  25676  itg2cnlem1  25684  limciun  25817  dvcnvlem  25902  dvivthlem2  25936  dvivth  25937  lhop1lem  25940  lhop1  25941  lhop2  25942  aalioulem3  26264  basellem3  27015  nodenselem8  27625  noseq0  28215  noseqp1  28216  noseqrdg0  28232  tgelrnln  28603  wlkiswwlks1  29840  ubthlem1  30842  pjrni  31674  pjoi0  31689  hmopidmchi  32123  hmopidmpji  32124  pjssdif1i  32147  dfpjop  32154  pjadj3  32160  elpjrn  32162  pjcmul1i  32173  pjcmul2i  32174  pj3si  32179  ofrn2  32614  prodindf  32836  mgcf1o  32976  cycpmfvlem  33073  cycpmfv1  33074  cycpmfv2  33075  locfinreflem  33845  cnre2csqlem  33915  elmrsubrn  35556  elmsubrn  35564  msubrn  35565  elmsta  35584  vhmcls  35602  mclsppslem  35619  neibastop2lem  36394  tailfb  36411  fvineqsneu  37445  ptrecube  37660  heicant  37695  mblfinlem2  37698  ftc1anclem7  37739  ftc1anc  37741  sstotbnd2  37814  prdsbnd  37833  heibor1lem  37849  heiborlem1  37851  dihcl  41309  dih0rn  41323  dih1dimatlem  41368  dihlspsnssN  41371  dochocss  41405  hdmaprnlem17N  41902  hgmaprnlem1N  41935  nacsfix  42745  kercvrlsm  43116  pwssplit4  43122  tfsconcatrev  43381  orbitinit  44989  orbitcl  44990  climinf  45646  climinf2lem  45744  limsupvaluz2  45776  supcnvlimsup  45778  fourierdlem25  46170  fourierdlem42  46187  fourierdlem54  46198  fourierdlem64  46208  fourierdlem65  46209  sge0le  46445  sge0seq  46484  imaelsetpreimafv  47426