Theorem fnfvelrn 7052

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5639   Fn wfn 6506  ‘cfv 6511

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  ffvelcdm  7053  fnfvelrnd  7054  fvcofneq  7065  fnovrn  7564  offvalfv  7675  fo1stres  7994  fo2ndres  7995  offsplitfpar  8098  fo2ndf  8100  seqomlem3  8420  seqomlem4  8421  phplem2  9169  indexfi  9311  dffi3  9382  ordtypelem7  9477  inf0  9574  infdifsn  9610  noinfep  9613  cantnflem3  9644  cantnf  9646  cardinfima  10050  alephfplem1  10057  alephfplem3  10059  alephfp  10061  dfac5  10082  dfac12lem2  10098  cfflb  10212  sornom  10230  fin23lem16  10288  fin23lem20  10290  isf32lem2  10307  axcc2lem  10389  axdc3lem2  10404  ttukeylem6  10467  konigthlem  10521  pwcfsdom  10536  pwfseqlem1  10611  gch2  10628  1nn  12197  peano2nn  12198  rpnnen1lem5  12940  om2uzrani  13917  uzrdglem  13922  uzrdg0i  13924  fseqsupubi  13943  ccatrn  14554  uzin2  15311  climsup  15636  ruclem12  16209  0ram  16991  setcepi  18050  acsmapd  18513  cycsubgcl  19138  ghmrn  19161  conjnmz  19184  pmtrrn  19387  sylow1lem4  19531  pgpssslw  19544  sylow2blem3  19552  sylow3lem2  19558  efgsfo  19669  gexex  19783  gsumval3eu  19834  gsumzsplit  19857  pjfo  21624  issubassa2  21801  mplbas2  21949  mpfconst  22008  mpfproj  22009  mpfind  22014  pf1const  22233  pf1id  22234  mpfpf1  22238  pf1mpf  22239  toprntopon  22812  cmpsub  23287  conncn  23313  2ndcctbss  23342  2ndcdisj  23343  2ndcsep  23346  iskgen2  23435  kgen2cn  23446  ptbasfi  23468  ptcnplem  23508  isr0  23624  r0cld  23625  zfbas  23783  uzrest  23784  rnelfm  23840  tmdgsum2  23983  evth  24858  bcth3  25231  ivthicc  25359  ovolmge0  25378  ovollb2lem  25389  ovolunlem1a  25397  ovoliunlem1  25403  ovoliun  25406  ovolicc2lem4  25421  voliunlem1  25451  voliunlem3  25453  volsup  25457  ioombl1lem2  25460  ioombl1lem4  25462  uniioombllem2  25484  uniioombllem3  25486  vitalilem2  25510  vitalilem4  25512  mbflimsup  25567  itg11  25592  i1faddlem  25594  i1fmullem  25595  itg1mulc  25605  i1fres  25606  itg1climres  25615  mbfi1fseqlem3  25618  itg2seq  25643  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2cnlem1  25662  limciun  25795  dvcnvlem  25880  dvivthlem2  25914  dvivth  25915  lhop1lem  25918  lhop1  25919  lhop2  25920  aalioulem3  26242  basellem3  26993  nodenselem8  27603  noseq0  28184  noseqp1  28185  noseqrdg0  28201  tgelrnln  28557  wlkiswwlks1  29797  ubthlem1  30799  pjrni  31631  pjoi0  31646  hmopidmchi  32080  hmopidmpji  32081  pjssdif1i  32104  dfpjop  32111  pjadj3  32117  elpjrn  32119  pjcmul1i  32130  pjcmul2i  32131  pj3si  32136  ofrn2  32564  prodindf  32786  mgcf1o  32929  cycpmfvlem  33069  cycpmfv1  33070  cycpmfv2  33071  locfinreflem  33830  cnre2csqlem  33900  elmrsubrn  35507  elmsubrn  35515  msubrn  35516  elmsta  35535  vhmcls  35553  mclsppslem  35570  neibastop2lem  36348  tailfb  36365  fvineqsneu  37399  ptrecube  37614  heicant  37649  mblfinlem2  37652  ftc1anclem7  37693  ftc1anc  37695  sstotbnd2  37768  prdsbnd  37787  heibor1lem  37803  heiborlem1  37805  dihcl  41264  dih0rn  41278  dih1dimatlem  41323  dihlspsnssN  41326  dochocss  41360  hdmaprnlem17N  41857  hgmaprnlem1N  41890  nacsfix  42700  kercvrlsm  43072  pwssplit4  43078  tfsconcatrev  43337  orbitinit  44946  orbitcl  44947  climinf  45604  climinf2lem  45704  limsupvaluz2  45736  supcnvlimsup  45738  fourierdlem25  46130  fourierdlem42  46147  fourierdlem54  46158  fourierdlem64  46168  fourierdlem65  46169  sge0le  46405  sge0seq  46444  imaelsetpreimafv  47396