Theorem fnfvelrn 7069

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ran crn 5655   Fn wfn 6525  ‘cfv 6530

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fn 6533  df-fv 6538

This theorem is referenced by:  ffvelcdm  7070  fnfvelrnd  7071  fvcofneq  7082  fnovrn  7580  offvalfv  7691  fo1stres  8012  fo2ndres  8013  offsplitfpar  8116  fo2ndf  8118  seqomlem3  8464  seqomlem4  8465  phplem2  9217  indexfi  9370  dffi3  9441  ordtypelem7  9536  inf0  9633  infdifsn  9669  noinfep  9672  cantnflem3  9703  cantnf  9705  cardinfima  10109  alephfplem1  10116  alephfplem3  10118  alephfp  10120  dfac5  10141  dfac12lem2  10157  cfflb  10271  sornom  10289  fin23lem16  10347  fin23lem20  10349  isf32lem2  10366  axcc2lem  10448  axdc3lem2  10463  ttukeylem6  10526  konigthlem  10580  pwcfsdom  10595  pwfseqlem1  10670  gch2  10687  1nn  12249  peano2nn  12250  rpnnen1lem5  12995  om2uzrani  13968  uzrdglem  13973  uzrdg0i  13975  fseqsupubi  13994  ccatrn  14605  uzin2  15361  climsup  15684  ruclem12  16257  0ram  17038  setcepi  18099  acsmapd  18562  cycsubgcl  19187  ghmrn  19210  conjnmz  19233  pmtrrn  19436  sylow1lem4  19580  pgpssslw  19593  sylow2blem3  19601  sylow3lem2  19607  efgsfo  19718  gexex  19832  gsumval3eu  19883  gsumzsplit  19906  pjfo  21673  issubassa2  21850  mplbas2  21998  mpfconst  22057  mpfproj  22058  mpfind  22063  pf1const  22282  pf1id  22283  mpfpf1  22287  pf1mpf  22288  toprntopon  22861  cmpsub  23336  conncn  23362  2ndcctbss  23391  2ndcdisj  23392  2ndcsep  23395  iskgen2  23484  kgen2cn  23495  ptbasfi  23517  ptcnplem  23557  isr0  23673  r0cld  23674  zfbas  23832  uzrest  23833  rnelfm  23889  tmdgsum2  24032  evth  24907  bcth3  25281  ivthicc  25409  ovolmge0  25428  ovollb2lem  25439  ovolunlem1a  25447  ovoliunlem1  25453  ovoliun  25456  ovolicc2lem4  25471  voliunlem1  25501  voliunlem3  25503  volsup  25507  ioombl1lem2  25510  ioombl1lem4  25512  uniioombllem2  25534  uniioombllem3  25536  vitalilem2  25560  vitalilem4  25562  mbflimsup  25617  itg11  25642  i1faddlem  25644  i1fmullem  25645  itg1mulc  25655  i1fres  25656  itg1climres  25665  mbfi1fseqlem3  25668  itg2seq  25693  itg2monolem2  25702  itg2monolem3  25703  itg2mono  25704  itg2cnlem1  25712  limciun  25845  dvcnvlem  25930  dvivthlem2  25964  dvivth  25965  lhop1lem  25968  lhop1  25969  lhop2  25970  aalioulem3  26292  basellem3  27043  nodenselem8  27653  noseq0  28213  noseqp1  28214  noseqrdg0  28230  tgelrnln  28555  wlkiswwlks1  29795  ubthlem1  30797  pjrni  31629  pjoi0  31644  hmopidmchi  32078  hmopidmpji  32079  pjssdif1i  32102  dfpjop  32109  pjadj3  32115  elpjrn  32117  pjcmul1i  32128  pjcmul2i  32129  pj3si  32134  ofrn2  32564  prodindf  32786  mgcf1o  32929  cycpmfvlem  33069  cycpmfv1  33070  cycpmfv2  33071  locfinreflem  33817  cnre2csqlem  33887  elmrsubrn  35488  elmsubrn  35496  msubrn  35497  elmsta  35516  vhmcls  35534  mclsppslem  35551  neibastop2lem  36324  tailfb  36341  fvineqsneu  37375  ptrecube  37590  heicant  37625  mblfinlem2  37628  ftc1anclem7  37669  ftc1anc  37671  sstotbnd2  37744  prdsbnd  37763  heibor1lem  37779  heiborlem1  37781  dihcl  41235  dih0rn  41249  dih1dimatlem  41294  dihlspsnssN  41297  dochocss  41331  hdmaprnlem17N  41828  hgmaprnlem1N  41861  nacsfix  42682  kercvrlsm  43054  pwssplit4  43060  tfsconcatrev  43319  orbitinit  44929  orbitcl  44930  climinf  45583  climinf2lem  45683  limsupvaluz2  45715  supcnvlimsup  45717  fourierdlem25  46109  fourierdlem42  46126  fourierdlem54  46137  fourierdlem64  46147  fourierdlem65  46148  sge0le  46384  sge0seq  46423  imaelsetpreimafv  47357