Theorem fnfvelrn 7026

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ran crn 5625   Fn wfn 6487  ‘cfv 6492

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 5231  ax-nul 5241  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  ffvelcdm  7027  fnfvelrnd  7028  fvcofneq  7039  fnovrn  7535  offvalfv  7646  fo1stres  7961  fo2ndres  7962  offsplitfpar  8062  fo2ndf  8064  seqomlem3  8384  seqomlem4  8385  phplem2  9132  indexfi  9263  dffi3  9337  ordtypelem7  9432  inf0  9533  infdifsn  9569  noinfep  9572  cantnflem3  9603  cantnf  9605  cardinfima  10010  alephfplem1  10017  alephfplem3  10019  alephfp  10021  dfac5  10042  dfac12lem2  10058  cfflb  10172  sornom  10190  fin23lem16  10248  fin23lem20  10250  isf32lem2  10267  axcc2lem  10349  axdc3lem2  10364  ttukeylem6  10427  konigthlem  10482  pwcfsdom  10497  pwfseqlem1  10572  gch2  10589  1nn  12176  peano2nn  12177  rpnnen1lem5  12922  om2uzrani  13905  uzrdglem  13910  uzrdg0i  13912  fseqsupubi  13931  ccatrn  14543  uzin2  15298  climsup  15623  ruclem12  16199  0ram  16982  setcepi  18046  acsmapd  18511  cycsubgcl  19172  ghmrn  19195  conjnmz  19218  pmtrrn  19423  sylow1lem4  19567  pgpssslw  19580  sylow2blem3  19588  sylow3lem2  19594  efgsfo  19705  gexex  19819  gsumval3eu  19870  gsumzsplit  19893  pjfo  21705  issubassa2  21882  mplbas2  22030  mpfconst  22097  mpfproj  22098  mpfind  22103  pf1const  22321  pf1id  22322  mpfpf1  22326  pf1mpf  22327  toprntopon  22900  cmpsub  23375  conncn  23401  2ndcctbss  23430  2ndcdisj  23431  2ndcsep  23434  iskgen2  23523  kgen2cn  23534  ptbasfi  23556  ptcnplem  23596  isr0  23712  r0cld  23713  zfbas  23871  uzrest  23872  rnelfm  23928  tmdgsum2  24071  evth  24936  bcth3  25308  ivthicc  25435  ovolmge0  25454  ovollb2lem  25465  ovolunlem1a  25473  ovoliunlem1  25479  ovoliun  25482  ovolicc2lem4  25497  voliunlem1  25527  voliunlem3  25529  volsup  25533  ioombl1lem2  25536  ioombl1lem4  25538  uniioombllem2  25560  uniioombllem3  25562  vitalilem2  25586  vitalilem4  25588  mbflimsup  25643  itg11  25668  i1faddlem  25670  i1fmullem  25671  itg1mulc  25681  i1fres  25682  itg1climres  25691  mbfi1fseqlem3  25694  itg2seq  25719  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  itg2cnlem1  25738  limciun  25871  dvcnvlem  25953  dvivthlem2  25986  dvivth  25987  lhop1lem  25990  lhop1  25991  lhop2  25992  aalioulem3  26311  basellem3  27060  nodenselem8  27669  noseq0  28296  noseqp1  28297  noseqrdg0  28313  tgelrnln  28712  wlkiswwlks1  29950  ubthlem1  30956  pjrni  31788  pjoi0  31803  hmopidmchi  32237  hmopidmpji  32238  pjssdif1i  32261  dfpjop  32268  pjadj3  32274  elpjrn  32276  pjcmul1i  32287  pjcmul2i  32288  pj3si  32293  ofrn2  32728  prodindf  32937  mgcf1o  33078  cycpmfvlem  33188  cycpmfv1  33189  cycpmfv2  33190  locfinreflem  34000  cnre2csqlem  34070  elmrsubrn  35718  elmsubrn  35726  msubrn  35727  elmsta  35746  vhmcls  35764  mclsppslem  35781  neibastop2lem  36558  tailfb  36575  fvineqsneu  37741  ptrecube  37955  heicant  37990  mblfinlem2  37993  ftc1anclem7  38034  ftc1anc  38036  sstotbnd2  38109  prdsbnd  38128  heibor1lem  38144  heiborlem1  38146  dihcl  41730  dih0rn  41744  dih1dimatlem  41789  dihlspsnssN  41792  dochocss  41826  hdmaprnlem17N  42323  hgmaprnlem1N  42356  nacsfix  43158  kercvrlsm  43529  pwssplit4  43535  tfsconcatrev  43794  orbitinit  45401  orbitcl  45402  climinf  46054  climinf2lem  46152  limsupvaluz2  46184  supcnvlimsup  46186  fourierdlem25  46578  fourierdlem42  46595  fourierdlem54  46606  fourierdlem64  46616  fourierdlem65  46617  sge0le  46853  sge0seq  46892  imaelsetpreimafv  47867