Theorem fnfvelrn 7095

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ran crn 5683   Fn wfn 6548  ‘cfv 6553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-iota 6505  df-fun 6555  df-fn 6556  df-fv 6561

This theorem is referenced by:  ffvelcdm  7096  fnfvelrnd  7097  fvcofneq  7108  fnovrn  7603  fo1stres  8027  fo2ndres  8028  offsplitfpar  8132  fo2ndf  8134  seqomlem3  8481  seqomlem4  8482  phplem2  9241  phplem4OLD  9253  indexfi  9394  dffi3  9464  ordtypelem7  9557  inf0  9654  infdifsn  9690  noinfep  9693  cantnflem3  9724  cantnf  9726  cardinfima  10130  alephfplem1  10137  alephfplem3  10139  alephfp  10141  dfac5  10161  dfac12lem2  10177  cfflb  10292  sornom  10310  fin23lem16  10368  fin23lem20  10370  isf32lem2  10387  axcc2lem  10469  axdc3lem2  10484  ttukeylem6  10547  konigthlem  10601  pwcfsdom  10616  pwfseqlem1  10691  gch2  10708  1nn  12263  peano2nn  12264  rpnnen1lem5  13005  om2uzrani  13959  uzrdglem  13964  uzrdg0i  13966  fseqsupubi  13985  ccatrn  14581  uzin2  15333  climsup  15658  ruclem12  16227  0ram  16998  setcepi  18086  acsmapd  18555  cycsubgcl  19175  ghmrn  19197  conjnmz  19220  pmtrrn  19426  sylow1lem4  19570  pgpssslw  19583  sylow2blem3  19591  sylow3lem2  19597  efgsfo  19708  gexex  19822  gsumval3eu  19873  gsumzsplit  19896  pjfo  21663  issubassa2  21839  mplbas2  21997  mpfconst  22064  mpfproj  22065  mpfind  22070  pf1const  22284  pf1id  22285  mpfpf1  22289  pf1mpf  22290  toprntopon  22855  cmpsub  23332  conncn  23358  2ndcctbss  23387  2ndcdisj  23388  2ndcsep  23391  iskgen2  23480  kgen2cn  23491  ptbasfi  23513  ptcnplem  23553  isr0  23669  r0cld  23670  zfbas  23828  uzrest  23829  rnelfm  23885  tmdgsum2  24028  evth  24913  bcth3  25287  ivthicc  25415  ovolmge0  25434  ovollb2lem  25445  ovolunlem1a  25453  ovoliunlem1  25459  ovoliun  25462  ovolicc2lem4  25477  voliunlem1  25507  voliunlem3  25509  volsup  25513  ioombl1lem2  25516  ioombl1lem4  25518  uniioombllem2  25540  uniioombllem3  25542  vitalilem2  25566  vitalilem4  25568  mbflimsup  25623  itg11  25648  i1faddlem  25650  i1fmullem  25651  itg1mulc  25662  i1fres  25663  itg1climres  25672  mbfi1fseqlem3  25675  itg2seq  25700  itg2monolem2  25709  itg2monolem3  25710  itg2mono  25711  itg2cnlem1  25719  limciun  25851  dvcnvlem  25936  dvivthlem2  25970  dvivth  25971  lhop1lem  25974  lhop1  25975  lhop2  25976  aalioulem3  26297  basellem3  27043  nodenselem8  27652  noseq0  28191  noseqp1  28192  noseqrdg0  28208  tgelrnln  28462  wlkiswwlks1  29706  ubthlem1  30708  pjrni  31540  pjoi0  31555  hmopidmchi  31989  hmopidmpji  31990  pjssdif1i  32013  dfpjop  32020  pjadj3  32026  elpjrn  32028  pjcmul1i  32039  pjcmul2i  32040  pj3si  32045  ofrn2  32455  mgcf1o  32759  cycpmfvlem  32862  cycpmfv1  32863  cycpmfv2  32864  locfinreflem  33482  cnre2csqlem  33552  prodindf  33683  elmrsubrn  35171  elmsubrn  35179  msubrn  35180  elmsta  35199  vhmcls  35217  mclsppslem  35234  neibastop2lem  35885  tailfb  35902  fvineqsneu  36931  ptrecube  37134  heicant  37169  mblfinlem2  37172  ftc1anclem7  37213  ftc1anc  37215  sstotbnd2  37288  prdsbnd  37307  heibor1lem  37323  heiborlem1  37325  dihcl  40783  dih0rn  40797  dih1dimatlem  40842  dihlspsnssN  40845  dochocss  40879  hdmaprnlem17N  41376  hgmaprnlem1N  41409  nacsfix  42181  kercvrlsm  42556  pwssplit4  42562  tfsconcatrev  42826  ssmapsn  44637  climinf  45041  climinf2lem  45141  limsupvaluz2  45173  supcnvlimsup  45175  fourierdlem25  45567  fourierdlem42  45584  fourierdlem54  45595  fourierdlem64  45605  fourierdlem65  45606  sge0le  45842  sge0seq  45881  imaelsetpreimafv  46782  offvalfv  47502