Theorem fnfvelrn 6842

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ran crn 5550   Fn wfn 6344  ‘cfv 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-iota 6308  df-fun 6351  df-fn 6352  df-fv 6357

This theorem is referenced by:  ffvelrn  6843  fvcofneq  6853  fnovrn  7317  fo1stres  7709  fo2ndres  7710  offsplitfpar  7809  fo2ndf  7811  seqomlem3  8082  seqomlem4  8083  phplem4  8693  indexfi  8826  dffi3  8889  ordtypelem7  8982  inf0  9078  infdifsn  9114  noinfep  9117  cantnflem3  9148  cantnf  9150  cardinfima  9517  alephfplem1  9524  alephfplem3  9526  alephfp  9528  dfac5  9548  dfac12lem2  9564  cfflb  9675  sornom  9693  fin23lem16  9751  fin23lem20  9753  isf32lem2  9770  axcc2lem  9852  axdc3lem2  9867  ttukeylem6  9930  konigthlem  9984  pwcfsdom  9999  pwfseqlem1  10074  gch2  10091  1nn  11643  peano2nn  11644  rpnnen1lem5  12374  om2uzrani  13314  uzrdglem  13319  uzrdg0i  13321  fseqsupubi  13340  ccatrn  13937  uzin2  14698  climsup  15020  ruclem12  15588  0ram  16350  setcepi  17342  acsmapd  17782  cycsubgcl  18343  ghmrn  18365  conjnmz  18386  pmtrrn  18579  sylow1lem4  18720  pgpssslw  18733  sylow2blem3  18741  sylow3lem2  18747  efgsfo  18859  gexex  18967  gsumval3eu  19018  gsumzsplit  19041  issubassa2  20115  mplbas2  20245  mpfconst  20308  mpfproj  20309  mpfind  20314  pf1const  20503  pf1id  20504  mpfpf1  20508  pf1mpf  20509  pjfo  20853  toprntopon  21527  cmpsub  22002  conncn  22028  2ndcctbss  22057  2ndcdisj  22058  2ndcsep  22061  iskgen2  22150  kgen2cn  22161  ptbasfi  22183  ptcnplem  22223  isr0  22339  r0cld  22340  zfbas  22498  uzrest  22499  rnelfm  22555  tmdgsum2  22698  evth  23557  bcth3  23928  ivthicc  24053  ovolmge0  24072  ovollb2lem  24083  ovolunlem1a  24091  ovoliunlem1  24097  ovoliun  24100  ovolicc2lem4  24115  voliunlem1  24145  voliunlem3  24147  volsup  24151  ioombl1lem2  24154  ioombl1lem4  24156  uniioombllem2  24178  uniioombllem3  24180  vitalilem2  24204  vitalilem4  24206  mbflimsup  24261  itg11  24286  i1faddlem  24288  i1fmullem  24289  itg1mulc  24299  i1fres  24300  itg1climres  24309  mbfi1fseqlem3  24312  itg2seq  24337  itg2monolem2  24346  itg2monolem3  24347  itg2mono  24348  itg2cnlem1  24356  limciun  24486  dvcnvlem  24567  dvivthlem2  24600  dvivth  24601  lhop1lem  24604  lhop1  24605  lhop2  24606  aalioulem3  24917  basellem3  25654  tgelrnln  26410  wlkiswwlks1  27639  ubthlem1  28641  pjrni  29473  pjoi0  29488  hmopidmchi  29922  hmopidmpji  29923  pjssdif1i  29946  dfpjop  29953  pjadj3  29959  elpjrn  29961  pjcmul1i  29972  pjcmul2i  29973  pj3si  29978  ofrn2  30381  cycpmfvlem  30749  cycpmfv1  30750  cycpmfv2  30751  locfinreflem  31099  cnre2csqlem  31148  prodindf  31277  elmrsubrn  32762  elmsubrn  32770  msubrn  32771  elmsta  32790  vhmcls  32808  mclsppslem  32825  nodenselem8  33190  neibastop2lem  33703  tailfb  33720  fvineqsneu  34686  ptrecube  34886  heicant  34921  mblfinlem2  34924  ftc1anclem7  34967  ftc1anc  34969  sstotbnd2  35046  prdsbnd  35065  heibor1lem  35081  heiborlem1  35083  dihcl  38400  dih0rn  38414  dih1dimatlem  38459  dihlspsnssN  38462  dochocss  38496  hdmaprnlem17N  38993  hgmaprnlem1N  39026  nacsfix  39302  kercvrlsm  39676  pwssplit4  39682  ssmapsn  41472  fnfvelrnd  41528  climinf  41880  climinf2lem  41980  limsupvaluz2  42012  supcnvlimsup  42014  fourierdlem25  42411  fourierdlem42  42428  fourierdlem54  42439  fourierdlem64  42449  fourierdlem65  42450  sge0le  42683  sge0seq  42722  imaelsetpreimafv  43549  offvalfv  44385