Theorem fnfvelrn 6940

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ran crn 5581   Fn wfn 6413  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-fv 6426

This theorem is referenced by:  ffvelrn  6941  fvcofneq  6951  fnovrn  7425  fo1stres  7830  fo2ndres  7831  offsplitfpar  7931  fo2ndf  7933  seqomlem3  8253  seqomlem4  8254  phplem4  8895  indexfi  9057  dffi3  9120  ordtypelem7  9213  inf0  9309  infdifsn  9345  noinfep  9348  cantnflem3  9379  cantnf  9381  cardinfima  9784  alephfplem1  9791  alephfplem3  9793  alephfp  9795  dfac5  9815  dfac12lem2  9831  cfflb  9946  sornom  9964  fin23lem16  10022  fin23lem20  10024  isf32lem2  10041  axcc2lem  10123  axdc3lem2  10138  ttukeylem6  10201  konigthlem  10255  pwcfsdom  10270  pwfseqlem1  10345  gch2  10362  1nn  11914  peano2nn  11915  rpnnen1lem5  12650  om2uzrani  13600  uzrdglem  13605  uzrdg0i  13607  fseqsupubi  13626  ccatrn  14222  uzin2  14984  climsup  15309  ruclem12  15878  0ram  16649  setcepi  17719  acsmapd  18187  cycsubgcl  18740  ghmrn  18762  conjnmz  18783  pmtrrn  18980  sylow1lem4  19121  pgpssslw  19134  sylow2blem3  19142  sylow3lem2  19148  efgsfo  19260  gexex  19369  gsumval3eu  19420  gsumzsplit  19443  pjfo  20832  issubassa2  21006  mplbas2  21153  mpfconst  21221  mpfproj  21222  mpfind  21227  pf1const  21422  pf1id  21423  mpfpf1  21427  pf1mpf  21428  toprntopon  21982  cmpsub  22459  conncn  22485  2ndcctbss  22514  2ndcdisj  22515  2ndcsep  22518  iskgen2  22607  kgen2cn  22618  ptbasfi  22640  ptcnplem  22680  isr0  22796  r0cld  22797  zfbas  22955  uzrest  22956  rnelfm  23012  tmdgsum2  23155  evth  24028  bcth3  24400  ivthicc  24527  ovolmge0  24546  ovollb2lem  24557  ovolunlem1a  24565  ovoliunlem1  24571  ovoliun  24574  ovolicc2lem4  24589  voliunlem1  24619  voliunlem3  24621  volsup  24625  ioombl1lem2  24628  ioombl1lem4  24630  uniioombllem2  24652  uniioombllem3  24654  vitalilem2  24678  vitalilem4  24680  mbflimsup  24735  itg11  24760  i1faddlem  24762  i1fmullem  24763  itg1mulc  24774  i1fres  24775  itg1climres  24784  mbfi1fseqlem3  24787  itg2seq  24812  itg2monolem2  24821  itg2monolem3  24822  itg2mono  24823  itg2cnlem1  24831  limciun  24963  dvcnvlem  25045  dvivthlem2  25078  dvivth  25079  lhop1lem  25082  lhop1  25083  lhop2  25084  aalioulem3  25399  basellem3  26137  tgelrnln  26895  wlkiswwlks1  28133  ubthlem1  29133  pjrni  29965  pjoi0  29980  hmopidmchi  30414  hmopidmpji  30415  pjssdif1i  30438  dfpjop  30445  pjadj3  30451  elpjrn  30453  pjcmul1i  30464  pjcmul2i  30465  pj3si  30470  ofrn2  30878  mgcf1o  31183  cycpmfvlem  31281  cycpmfv1  31282  cycpmfv2  31283  locfinreflem  31692  cnre2csqlem  31762  prodindf  31891  elmrsubrn  33382  elmsubrn  33390  msubrn  33391  elmsta  33410  vhmcls  33428  mclsppslem  33445  nodenselem8  33821  neibastop2lem  34476  tailfb  34493  fvineqsneu  35509  ptrecube  35704  heicant  35739  mblfinlem2  35742  ftc1anclem7  35783  ftc1anc  35785  sstotbnd2  35859  prdsbnd  35878  heibor1lem  35894  heiborlem1  35896  dihcl  39211  dih0rn  39225  dih1dimatlem  39270  dihlspsnssN  39273  dochocss  39307  hdmaprnlem17N  39804  hgmaprnlem1N  39837  nacsfix  40450  kercvrlsm  40824  pwssplit4  40830  ssmapsn  42645  fnfvelrnd  42697  climinf  43037  climinf2lem  43137  limsupvaluz2  43169  supcnvlimsup  43171  fourierdlem25  43563  fourierdlem42  43580  fourierdlem54  43591  fourierdlem64  43601  fourierdlem65  43602  sge0le  43835  sge0seq  43874  imaelsetpreimafv  44735  offvalfv  45566