Theorem fnfvelrn 6713

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2081  ran crn 5444   Fn wfn 6220  ‘cfv 6225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-iota 6189  df-fun 6227  df-fn 6228  df-fv 6233

This theorem is referenced by:  ffvelrn  6714  fvcofneq  6724  fnovrn  7179  fo1stres  7571  fo2ndres  7572  fo2ndf  7670  seqomlem3  7939  seqomlem4  7940  phplem4  8546  indexfi  8678  dffi3  8741  ordtypelem7  8834  inf0  8930  infdifsn  8966  noinfep  8969  cantnflem3  9000  cantnf  9002  cardinfima  9369  alephfplem1  9376  alephfplem3  9378  alephfp  9380  dfac5  9400  dfac12lem2  9416  cfflb  9527  sornom  9545  fin23lem16  9603  fin23lem20  9605  isf32lem2  9622  axcc2lem  9704  axdc3lem2  9719  ttukeylem6  9782  konigthlem  9836  pwcfsdom  9851  pwfseqlem1  9926  gch2  9943  1nn  11497  peano2nn  11498  rpnnen1lem5  12230  om2uzrani  13170  uzrdglem  13175  uzrdg0i  13177  fseqsupubi  13196  ccatrn  13787  uzin2  14538  climsup  14860  ruclem12  15427  0ram  16185  setcepi  17177  acsmapd  17617  cycsubgcl  18059  ghmrn  18112  conjnmz  18133  pmtrrn  18316  sylow1lem4  18456  pgpssslw  18469  sylow2blem3  18477  sylow3lem2  18483  efgsfo  18592  gexex  18696  gsumval3eu  18745  gsumzsplit  18767  issubassa2  19813  mplbas2  19938  mpfconst  19997  mpfproj  19998  mpfind  20003  pf1const  20191  pf1id  20192  mpfpf1  20196  pf1mpf  20197  pjfo  20541  toprntopon  21217  cmpsub  21692  conncn  21718  2ndcctbss  21747  2ndcdisj  21748  2ndcsep  21751  iskgen2  21840  kgen2cn  21851  ptbasfi  21873  ptcnplem  21913  isr0  22029  r0cld  22030  zfbas  22188  uzrest  22189  rnelfm  22245  tmdgsum2  22388  evth  23246  bcth3  23617  ivthicc  23742  ovolmge0  23761  ovollb2lem  23772  ovolunlem1a  23780  ovoliunlem1  23786  ovoliun  23789  ovolicc2lem4  23804  voliunlem1  23834  voliunlem3  23836  volsup  23840  ioombl1lem2  23843  ioombl1lem4  23845  uniioombllem2  23867  uniioombllem3  23869  vitalilem2  23893  vitalilem4  23895  mbflimsup  23950  itg11  23975  i1faddlem  23977  i1fmullem  23978  itg1mulc  23988  i1fres  23989  itg1climres  23998  mbfi1fseqlem3  24001  itg2seq  24026  itg2monolem2  24035  itg2monolem3  24036  itg2mono  24037  itg2cnlem1  24045  limciun  24175  dvcnvlem  24256  dvivthlem2  24289  dvivth  24290  lhop1lem  24293  lhop1  24294  lhop2  24295  aalioulem3  24606  basellem3  25342  tgelrnln  26098  wlkiswwlks1  27332  ubthlem1  28338  pjrni  29170  pjoi0  29185  hmopidmchi  29619  hmopidmpji  29620  pjssdif1i  29643  dfpjop  29650  pjadj3  29656  elpjrn  29658  pjcmul1i  29669  pjcmul2i  29670  pj3si  29675  ofrn2  30077  cycpmfvlem  30401  cycpmfv1  30402  cycpmfv2  30403  locfinreflem  30721  cnre2csqlem  30770  prodindf  30899  elmrsubrn  32375  elmsubrn  32383  msubrn  32384  elmsta  32403  vhmcls  32421  mclsppslem  32438  nodenselem8  32804  neibastop2lem  33317  tailfb  33334  fvineqsneu  34223  ptrecube  34423  heicant  34458  mblfinlem2  34461  ftc1anclem7  34504  ftc1anc  34506  sstotbnd2  34584  prdsbnd  34603  heibor1lem  34619  heiborlem1  34621  dihcl  37937  dih0rn  37951  dih1dimatlem  37996  dihlspsnssN  37999  dochocss  38033  hdmaprnlem17N  38530  hgmaprnlem1N  38563  nacsfix  38794  kercvrlsm  39168  pwssplit4  39174  ssmapsn  41019  fnfvelrnd  41076  climinf  41429  climinf2lem  41529  limsupvaluz2  41561  supcnvlimsup  41563  fourierdlem25  41959  fourierdlem42  41976  fourierdlem54  41987  fourierdlem64  41997  fourierdlem65  41998  sge0le  42231  sge0seq  42270  offvalfv  43869