Theorem fnfvelrn 7022

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ran crn 5622   Fn wfn 6484  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by:  ffvelcdm  7023  fnfvelrnd  7024  fvcofneq  7035  fnovrn  7530  offvalfv  7641  fo1stres  7956  fo2ndres  7957  offsplitfpar  8058  fo2ndf  8060  seqomlem3  8380  seqomlem4  8381  phplem2  9125  indexfi  9255  dffi3  9326  ordtypelem7  9421  inf0  9522  infdifsn  9558  noinfep  9561  cantnflem3  9592  cantnf  9594  cardinfima  9999  alephfplem1  10006  alephfplem3  10008  alephfp  10010  dfac5  10031  dfac12lem2  10047  cfflb  10161  sornom  10179  fin23lem16  10237  fin23lem20  10239  isf32lem2  10256  axcc2lem  10338  axdc3lem2  10353  ttukeylem6  10416  konigthlem  10470  pwcfsdom  10485  pwfseqlem1  10560  gch2  10577  1nn  12147  peano2nn  12148  rpnnen1lem5  12885  om2uzrani  13866  uzrdglem  13871  uzrdg0i  13873  fseqsupubi  13892  ccatrn  14504  uzin2  15259  climsup  15584  ruclem12  16157  0ram  16939  setcepi  18003  acsmapd  18468  cycsubgcl  19126  ghmrn  19149  conjnmz  19172  pmtrrn  19377  sylow1lem4  19521  pgpssslw  19534  sylow2blem3  19542  sylow3lem2  19548  efgsfo  19659  gexex  19773  gsumval3eu  19824  gsumzsplit  19847  pjfo  21661  issubassa2  21839  mplbas2  21988  mpfconst  22055  mpfproj  22056  mpfind  22061  pf1const  22281  pf1id  22282  mpfpf1  22286  pf1mpf  22287  toprntopon  22860  cmpsub  23335  conncn  23361  2ndcctbss  23390  2ndcdisj  23391  2ndcsep  23394  iskgen2  23483  kgen2cn  23494  ptbasfi  23516  ptcnplem  23556  isr0  23672  r0cld  23673  zfbas  23831  uzrest  23832  rnelfm  23888  tmdgsum2  24031  evth  24905  bcth3  25278  ivthicc  25406  ovolmge0  25425  ovollb2lem  25436  ovolunlem1a  25444  ovoliunlem1  25450  ovoliun  25453  ovolicc2lem4  25468  voliunlem1  25498  voliunlem3  25500  volsup  25504  ioombl1lem2  25507  ioombl1lem4  25509  uniioombllem2  25531  uniioombllem3  25533  vitalilem2  25557  vitalilem4  25559  mbflimsup  25614  itg11  25639  i1faddlem  25641  i1fmullem  25642  itg1mulc  25652  i1fres  25653  itg1climres  25662  mbfi1fseqlem3  25665  itg2seq  25690  itg2monolem2  25699  itg2monolem3  25700  itg2mono  25701  itg2cnlem1  25709  limciun  25842  dvcnvlem  25927  dvivthlem2  25961  dvivth  25962  lhop1lem  25965  lhop1  25966  lhop2  25967  aalioulem3  26289  basellem3  27040  nodenselem8  27650  noseq0  28240  noseqp1  28241  noseqrdg0  28257  tgelrnln  28628  wlkiswwlks1  29866  ubthlem1  30871  pjrni  31703  pjoi0  31718  hmopidmchi  32152  hmopidmpji  32153  pjssdif1i  32176  dfpjop  32183  pjadj3  32189  elpjrn  32191  pjcmul1i  32202  pjcmul2i  32203  pj3si  32208  ofrn2  32644  prodindf  32872  mgcf1o  33013  cycpmfvlem  33122  cycpmfv1  33123  cycpmfv2  33124  locfinreflem  33925  cnre2csqlem  33995  elmrsubrn  35636  elmsubrn  35644  msubrn  35645  elmsta  35664  vhmcls  35682  mclsppslem  35699  neibastop2lem  36476  tailfb  36493  fvineqsneu  37528  ptrecube  37733  heicant  37768  mblfinlem2  37771  ftc1anclem7  37812  ftc1anc  37814  sstotbnd2  37887  prdsbnd  37906  heibor1lem  37922  heiborlem1  37924  dihcl  41442  dih0rn  41456  dih1dimatlem  41501  dihlspsnssN  41504  dochocss  41538  hdmaprnlem17N  42035  hgmaprnlem1N  42068  nacsfix  42869  kercvrlsm  43240  pwssplit4  43246  tfsconcatrev  43505  orbitinit  45113  orbitcl  45114  climinf  45768  climinf2lem  45866  limsupvaluz2  45898  supcnvlimsup  45900  fourierdlem25  46292  fourierdlem42  46309  fourierdlem54  46320  fourierdlem64  46330  fourierdlem65  46331  sge0le  46567  sge0seq  46606  imaelsetpreimafv  47557