Theorem fnfvelrn 6850

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ran crn 5558   Fn wfn 6352  ‘cfv 6357

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fn 6360  df-fv 6365

This theorem is referenced by:  ffvelrn  6851  fvcofneq  6861  fnovrn  7325  fo1stres  7717  fo2ndres  7718  offsplitfpar  7817  fo2ndf  7819  seqomlem3  8090  seqomlem4  8091  phplem4  8701  indexfi  8834  dffi3  8897  ordtypelem7  8990  inf0  9086  infdifsn  9122  noinfep  9125  cantnflem3  9156  cantnf  9158  cardinfima  9525  alephfplem1  9532  alephfplem3  9534  alephfp  9536  dfac5  9556  dfac12lem2  9572  cfflb  9683  sornom  9701  fin23lem16  9759  fin23lem20  9761  isf32lem2  9778  axcc2lem  9860  axdc3lem2  9875  ttukeylem6  9938  konigthlem  9992  pwcfsdom  10007  pwfseqlem1  10082  gch2  10099  1nn  11651  peano2nn  11652  rpnnen1lem5  12383  om2uzrani  13323  uzrdglem  13328  uzrdg0i  13330  fseqsupubi  13349  ccatrn  13945  uzin2  14706  climsup  15028  ruclem12  15596  0ram  16358  setcepi  17350  acsmapd  17790  cycsubgcl  18351  ghmrn  18373  conjnmz  18394  pmtrrn  18587  sylow1lem4  18728  pgpssslw  18741  sylow2blem3  18749  sylow3lem2  18755  efgsfo  18867  gexex  18975  gsumval3eu  19026  gsumzsplit  19049  issubassa2  20123  mplbas2  20253  mpfconst  20316  mpfproj  20317  mpfind  20322  pf1const  20511  pf1id  20512  mpfpf1  20516  pf1mpf  20517  pjfo  20861  toprntopon  21535  cmpsub  22010  conncn  22036  2ndcctbss  22065  2ndcdisj  22066  2ndcsep  22069  iskgen2  22158  kgen2cn  22169  ptbasfi  22191  ptcnplem  22231  isr0  22347  r0cld  22348  zfbas  22506  uzrest  22507  rnelfm  22563  tmdgsum2  22706  evth  23565  bcth3  23936  ivthicc  24061  ovolmge0  24080  ovollb2lem  24091  ovolunlem1a  24099  ovoliunlem1  24105  ovoliun  24108  ovolicc2lem4  24123  voliunlem1  24153  voliunlem3  24155  volsup  24159  ioombl1lem2  24162  ioombl1lem4  24164  uniioombllem2  24186  uniioombllem3  24188  vitalilem2  24212  vitalilem4  24214  mbflimsup  24269  itg11  24294  i1faddlem  24296  i1fmullem  24297  itg1mulc  24307  i1fres  24308  itg1climres  24317  mbfi1fseqlem3  24320  itg2seq  24345  itg2monolem2  24354  itg2monolem3  24355  itg2mono  24356  itg2cnlem1  24364  limciun  24494  dvcnvlem  24575  dvivthlem2  24608  dvivth  24609  lhop1lem  24612  lhop1  24613  lhop2  24614  aalioulem3  24925  basellem3  25662  tgelrnln  26418  wlkiswwlks1  27647  ubthlem1  28649  pjrni  29481  pjoi0  29496  hmopidmchi  29930  hmopidmpji  29931  pjssdif1i  29954  dfpjop  29961  pjadj3  29967  elpjrn  29969  pjcmul1i  29980  pjcmul2i  29981  pj3si  29986  ofrn2  30389  cycpmfvlem  30756  cycpmfv1  30757  cycpmfv2  30758  locfinreflem  31106  cnre2csqlem  31155  prodindf  31284  elmrsubrn  32769  elmsubrn  32777  msubrn  32778  elmsta  32797  vhmcls  32815  mclsppslem  32832  nodenselem8  33197  neibastop2lem  33710  tailfb  33727  fvineqsneu  34694  ptrecube  34894  heicant  34929  mblfinlem2  34932  ftc1anclem7  34975  ftc1anc  34977  sstotbnd2  35054  prdsbnd  35073  heibor1lem  35089  heiborlem1  35091  dihcl  38408  dih0rn  38422  dih1dimatlem  38467  dihlspsnssN  38470  dochocss  38504  hdmaprnlem17N  39001  hgmaprnlem1N  39034  nacsfix  39316  kercvrlsm  39690  pwssplit4  39696  ssmapsn  41486  fnfvelrnd  41542  climinf  41894  climinf2lem  41994  limsupvaluz2  42026  supcnvlimsup  42028  fourierdlem25  42424  fourierdlem42  42441  fourierdlem54  42452  fourierdlem64  42462  fourierdlem65  42463  sge0le  42696  sge0seq  42735  imaelsetpreimafv  43562  offvalfv  44398