Theorem fnfvelrn 7079

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ran crn 5676   Fn wfn 6535  ‘cfv 6540

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is referenced by:  ffvelcdm  7080  fnfvelrnd  7081  fvcofneq  7091  fnovrn  7578  fo1stres  7997  fo2ndres  7998  offsplitfpar  8101  fo2ndf  8103  seqomlem3  8448  seqomlem4  8449  phplem2  9204  phplem4OLD  9216  indexfi  9356  dffi3  9422  ordtypelem7  9515  inf0  9612  infdifsn  9648  noinfep  9651  cantnflem3  9682  cantnf  9684  cardinfima  10088  alephfplem1  10095  alephfplem3  10097  alephfp  10099  dfac5  10119  dfac12lem2  10135  cfflb  10250  sornom  10268  fin23lem16  10326  fin23lem20  10328  isf32lem2  10345  axcc2lem  10427  axdc3lem2  10442  ttukeylem6  10505  konigthlem  10559  pwcfsdom  10574  pwfseqlem1  10649  gch2  10666  1nn  12219  peano2nn  12220  rpnnen1lem5  12961  om2uzrani  13913  uzrdglem  13918  uzrdg0i  13920  fseqsupubi  13939  ccatrn  14535  uzin2  15287  climsup  15612  ruclem12  16180  0ram  16949  setcepi  18034  acsmapd  18503  cycsubgcl  19077  ghmrn  19099  conjnmz  19120  pmtrrn  19319  sylow1lem4  19463  pgpssslw  19476  sylow2blem3  19484  sylow3lem2  19490  efgsfo  19601  gexex  19715  gsumval3eu  19766  gsumzsplit  19789  pjfo  21261  issubassa2  21437  mplbas2  21588  mpfconst  21655  mpfproj  21656  mpfind  21661  pf1const  21856  pf1id  21857  mpfpf1  21861  pf1mpf  21862  toprntopon  22418  cmpsub  22895  conncn  22921  2ndcctbss  22950  2ndcdisj  22951  2ndcsep  22954  iskgen2  23043  kgen2cn  23054  ptbasfi  23076  ptcnplem  23116  isr0  23232  r0cld  23233  zfbas  23391  uzrest  23392  rnelfm  23448  tmdgsum2  23591  evth  24466  bcth3  24839  ivthicc  24966  ovolmge0  24985  ovollb2lem  24996  ovolunlem1a  25004  ovoliunlem1  25010  ovoliun  25013  ovolicc2lem4  25028  voliunlem1  25058  voliunlem3  25060  volsup  25064  ioombl1lem2  25067  ioombl1lem4  25069  uniioombllem2  25091  uniioombllem3  25093  vitalilem2  25117  vitalilem4  25119  mbflimsup  25174  itg11  25199  i1faddlem  25201  i1fmullem  25202  itg1mulc  25213  i1fres  25214  itg1climres  25223  mbfi1fseqlem3  25226  itg2seq  25251  itg2monolem2  25260  itg2monolem3  25261  itg2mono  25262  itg2cnlem1  25270  limciun  25402  dvcnvlem  25484  dvivthlem2  25517  dvivth  25518  lhop1lem  25521  lhop1  25522  lhop2  25523  aalioulem3  25838  basellem3  26576  nodenselem8  27183  tgelrnln  27870  wlkiswwlks1  29110  ubthlem1  30110  pjrni  30942  pjoi0  30957  hmopidmchi  31391  hmopidmpji  31392  pjssdif1i  31415  dfpjop  31422  pjadj3  31428  elpjrn  31430  pjcmul1i  31441  pjcmul2i  31442  pj3si  31447  ofrn2  31852  mgcf1o  32160  cycpmfvlem  32258  cycpmfv1  32259  cycpmfv2  32260  locfinreflem  32808  cnre2csqlem  32878  prodindf  33009  elmrsubrn  34499  elmsubrn  34507  msubrn  34508  elmsta  34527  vhmcls  34545  mclsppslem  34562  neibastop2lem  35233  tailfb  35250  fvineqsneu  36280  ptrecube  36476  heicant  36511  mblfinlem2  36514  ftc1anclem7  36555  ftc1anc  36557  sstotbnd2  36630  prdsbnd  36649  heibor1lem  36665  heiborlem1  36667  dihcl  40129  dih0rn  40143  dih1dimatlem  40188  dihlspsnssN  40191  dochocss  40225  hdmaprnlem17N  40722  hgmaprnlem1N  40755  nacsfix  41435  kercvrlsm  41810  pwssplit4  41816  tfsconcatrev  42083  ssmapsn  43900  climinf  44308  climinf2lem  44408  limsupvaluz2  44440  supcnvlimsup  44442  fourierdlem25  44834  fourierdlem42  44851  fourierdlem54  44862  fourierdlem64  44872  fourierdlem65  44873  sge0le  45109  sge0seq  45148  imaelsetpreimafv  46049  offvalfv  46971