Theorem fnfvelrn 7100

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ran crn 5686   Fn wfn 6556  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569

This theorem is referenced by:  ffvelcdm  7101  fnfvelrnd  7102  fvcofneq  7113  fnovrn  7608  offvalfv  7719  fo1stres  8040  fo2ndres  8041  offsplitfpar  8144  fo2ndf  8146  seqomlem3  8492  seqomlem4  8493  phplem2  9245  phplem4OLD  9257  indexfi  9400  dffi3  9471  ordtypelem7  9564  inf0  9661  infdifsn  9697  noinfep  9700  cantnflem3  9731  cantnf  9733  cardinfima  10137  alephfplem1  10144  alephfplem3  10146  alephfp  10148  dfac5  10169  dfac12lem2  10185  cfflb  10299  sornom  10317  fin23lem16  10375  fin23lem20  10377  isf32lem2  10394  axcc2lem  10476  axdc3lem2  10491  ttukeylem6  10554  konigthlem  10608  pwcfsdom  10623  pwfseqlem1  10698  gch2  10715  1nn  12277  peano2nn  12278  rpnnen1lem5  13023  om2uzrani  13993  uzrdglem  13998  uzrdg0i  14000  fseqsupubi  14019  ccatrn  14627  uzin2  15383  climsup  15706  ruclem12  16277  0ram  17058  setcepi  18133  acsmapd  18599  cycsubgcl  19224  ghmrn  19247  conjnmz  19270  pmtrrn  19475  sylow1lem4  19619  pgpssslw  19632  sylow2blem3  19640  sylow3lem2  19646  efgsfo  19757  gexex  19871  gsumval3eu  19922  gsumzsplit  19945  pjfo  21735  issubassa2  21912  mplbas2  22060  mpfconst  22125  mpfproj  22126  mpfind  22131  pf1const  22350  pf1id  22351  mpfpf1  22355  pf1mpf  22356  toprntopon  22931  cmpsub  23408  conncn  23434  2ndcctbss  23463  2ndcdisj  23464  2ndcsep  23467  iskgen2  23556  kgen2cn  23567  ptbasfi  23589  ptcnplem  23629  isr0  23745  r0cld  23746  zfbas  23904  uzrest  23905  rnelfm  23961  tmdgsum2  24104  evth  24991  bcth3  25365  ivthicc  25493  ovolmge0  25512  ovollb2lem  25523  ovolunlem1a  25531  ovoliunlem1  25537  ovoliun  25540  ovolicc2lem4  25555  voliunlem1  25585  voliunlem3  25587  volsup  25591  ioombl1lem2  25594  ioombl1lem4  25596  uniioombllem2  25618  uniioombllem3  25620  vitalilem2  25644  vitalilem4  25646  mbflimsup  25701  itg11  25726  i1faddlem  25728  i1fmullem  25729  itg1mulc  25739  i1fres  25740  itg1climres  25749  mbfi1fseqlem3  25752  itg2seq  25777  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2cnlem1  25796  limciun  25929  dvcnvlem  26014  dvivthlem2  26048  dvivth  26049  lhop1lem  26052  lhop1  26053  lhop2  26054  aalioulem3  26376  basellem3  27126  nodenselem8  27736  noseq0  28296  noseqp1  28297  noseqrdg0  28313  tgelrnln  28638  wlkiswwlks1  29887  ubthlem1  30889  pjrni  31721  pjoi0  31736  hmopidmchi  32170  hmopidmpji  32171  pjssdif1i  32194  dfpjop  32201  pjadj3  32207  elpjrn  32209  pjcmul1i  32220  pjcmul2i  32221  pj3si  32226  ofrn2  32650  prodindf  32848  mgcf1o  32993  cycpmfvlem  33132  cycpmfv1  33133  cycpmfv2  33134  locfinreflem  33839  cnre2csqlem  33909  elmrsubrn  35525  elmsubrn  35533  msubrn  35534  elmsta  35553  vhmcls  35571  mclsppslem  35588  neibastop2lem  36361  tailfb  36378  fvineqsneu  37412  ptrecube  37627  heicant  37662  mblfinlem2  37665  ftc1anclem7  37706  ftc1anc  37708  sstotbnd2  37781  prdsbnd  37800  heibor1lem  37816  heiborlem1  37818  dihcl  41272  dih0rn  41286  dih1dimatlem  41331  dihlspsnssN  41334  dochocss  41368  hdmaprnlem17N  41865  hgmaprnlem1N  41898  nacsfix  42723  kercvrlsm  43095  pwssplit4  43101  tfsconcatrev  43361  climinf  45621  climinf2lem  45721  limsupvaluz2  45753  supcnvlimsup  45755  fourierdlem25  46147  fourierdlem42  46164  fourierdlem54  46175  fourierdlem64  46185  fourierdlem65  46186  sge0le  46422  sge0seq  46461  imaelsetpreimafv  47382