Theorem fnfvelrn 7014

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5620   Fn wfn 6477  ‘cfv 6482

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-fv 6490

This theorem is referenced by:  ffvelcdm  7015  fnfvelrnd  7016  fvcofneq  7027  fnovrn  7524  offvalfv  7635  fo1stres  7950  fo2ndres  7951  offsplitfpar  8052  fo2ndf  8054  seqomlem3  8374  seqomlem4  8375  phplem2  9119  indexfi  9250  dffi3  9321  ordtypelem7  9416  inf0  9517  infdifsn  9553  noinfep  9556  cantnflem3  9587  cantnf  9589  cardinfima  9991  alephfplem1  9998  alephfplem3  10000  alephfp  10002  dfac5  10023  dfac12lem2  10039  cfflb  10153  sornom  10171  fin23lem16  10229  fin23lem20  10231  isf32lem2  10248  axcc2lem  10330  axdc3lem2  10345  ttukeylem6  10408  konigthlem  10462  pwcfsdom  10477  pwfseqlem1  10552  gch2  10569  1nn  12139  peano2nn  12140  rpnnen1lem5  12882  om2uzrani  13859  uzrdglem  13864  uzrdg0i  13866  fseqsupubi  13885  ccatrn  14496  uzin2  15252  climsup  15577  ruclem12  16150  0ram  16932  setcepi  17995  acsmapd  18460  cycsubgcl  19085  ghmrn  19108  conjnmz  19131  pmtrrn  19336  sylow1lem4  19480  pgpssslw  19493  sylow2blem3  19501  sylow3lem2  19507  efgsfo  19618  gexex  19732  gsumval3eu  19783  gsumzsplit  19806  pjfo  21622  issubassa2  21799  mplbas2  21947  mpfconst  22006  mpfproj  22007  mpfind  22012  pf1const  22231  pf1id  22232  mpfpf1  22236  pf1mpf  22237  toprntopon  22810  cmpsub  23285  conncn  23311  2ndcctbss  23340  2ndcdisj  23341  2ndcsep  23344  iskgen2  23433  kgen2cn  23444  ptbasfi  23466  ptcnplem  23506  isr0  23622  r0cld  23623  zfbas  23781  uzrest  23782  rnelfm  23838  tmdgsum2  23981  evth  24856  bcth3  25229  ivthicc  25357  ovolmge0  25376  ovollb2lem  25387  ovolunlem1a  25395  ovoliunlem1  25401  ovoliun  25404  ovolicc2lem4  25419  voliunlem1  25449  voliunlem3  25451  volsup  25455  ioombl1lem2  25458  ioombl1lem4  25460  uniioombllem2  25482  uniioombllem3  25484  vitalilem2  25508  vitalilem4  25510  mbflimsup  25565  itg11  25590  i1faddlem  25592  i1fmullem  25593  itg1mulc  25603  i1fres  25604  itg1climres  25613  mbfi1fseqlem3  25616  itg2seq  25641  itg2monolem2  25650  itg2monolem3  25651  itg2mono  25652  itg2cnlem1  25660  limciun  25793  dvcnvlem  25878  dvivthlem2  25912  dvivth  25913  lhop1lem  25916  lhop1  25917  lhop2  25918  aalioulem3  26240  basellem3  26991  nodenselem8  27601  noseq0  28189  noseqp1  28190  noseqrdg0  28206  tgelrnln  28575  wlkiswwlks1  29812  ubthlem1  30814  pjrni  31646  pjoi0  31661  hmopidmchi  32095  hmopidmpji  32096  pjssdif1i  32119  dfpjop  32126  pjadj3  32132  elpjrn  32134  pjcmul1i  32145  pjcmul2i  32146  pj3si  32151  ofrn2  32583  prodindf  32806  mgcf1o  32945  cycpmfvlem  33054  cycpmfv1  33055  cycpmfv2  33056  locfinreflem  33807  cnre2csqlem  33877  elmrsubrn  35493  elmsubrn  35501  msubrn  35502  elmsta  35521  vhmcls  35539  mclsppslem  35556  neibastop2lem  36334  tailfb  36351  fvineqsneu  37385  ptrecube  37600  heicant  37635  mblfinlem2  37638  ftc1anclem7  37679  ftc1anc  37681  sstotbnd2  37754  prdsbnd  37773  heibor1lem  37789  heiborlem1  37791  dihcl  41249  dih0rn  41263  dih1dimatlem  41308  dihlspsnssN  41311  dochocss  41345  hdmaprnlem17N  41842  hgmaprnlem1N  41875  nacsfix  42685  kercvrlsm  43056  pwssplit4  43062  tfsconcatrev  43321  orbitinit  44930  orbitcl  44931  climinf  45587  climinf2lem  45687  limsupvaluz2  45719  supcnvlimsup  45721  fourierdlem25  46113  fourierdlem42  46130  fourierdlem54  46141  fourierdlem64  46151  fourierdlem65  46152  sge0le  46388  sge0seq  46427  imaelsetpreimafv  47379