Theorem fnfvelrn 7080

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ran crn 5652   Fn wfn 6533  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  ffvelcdm  7081  fnfvelrnd  7082  fvcofneq  7093  fnovrn  7596  offvalfv  7715  fo1stres  8027  fo2ndres  8028  offsplitfpar  8130  fo2ndf  8132  seqomlem3  8462  seqomlem4  8463  phplem2  9220  indexfi  9349  dffi3  9423  ordtypelem7  9518  inf0  9622  infdifsn  9658  noinfep  9661  cantnflem3  9692  cantnf  9694  cardinfima  10176  alephfplem1  10183  alephfplem3  10185  alephfp  10187  dfac5  10207  dfac12lem2  10223  cfflb  10337  sornom  10355  fin23lem16  10413  fin23lem20  10415  isf32lem2  10432  axcc2lem  10514  axdc3lem2  10529  ttukeylem6  10592  konigthlem  10653  pwcfsdom  10668  pwfseqlem1  10743  gch2  10760  1nn  12346  peano2nn  12347  rpnnen1lem5  13109  om2uzrani  14095  uzrdglem  14100  uzrdg0i  14102  fseqsupubi  14121  ccatrn  14735  sgnrn  15251  uzin2  15512  climsup  15837  ruclem12  16409  0ram  17198  setcepi  18263  acsmapd  18728  cycsubgcl  19421  ghmrn  19443  conjnmz  19466  pmtrrn  19671  sylow1lem4  19815  pgpssslw  19828  sylow2blem3  19836  sylow3lem2  19842  efgsfo  19953  gexex  20067  gsumval3eu  20118  gsumzsplit  20141  pjfo  22021  issubassa2  22200  mplbas2  22351  mpfconst  22418  mpfproj  22419  mpfind  22424  pf1const  22664  pf1id  22665  mpfpf1  22669  pf1mpf  22670  toprntopon  23243  cmpsub  23718  conncn  23744  2ndcctbss  23774  2ndcdisj  23775  2ndcsep  23778  iskgen2  23867  kgen2cn  23878  ptbasfi  23900  ptcnplem  23940  isr0  24056  r0cld  24057  zfbas  24215  uzrest  24216  rnelfm  24272  tmdgsum2  24415  evth  25280  bcth3  25652  ivthicc  25779  ovolmge0  25798  ovollb2lem  25809  ovolunlem1a  25817  ovoliunlem1  25823  ovoliun  25826  ovolicc2lem4  25841  voliunlem1  25871  voliunlem3  25873  volsup  25877  ioombl1lem2  25880  ioombl1lem4  25882  uniioombllem2  25904  uniioombllem3  25906  vitalilem2  25930  vitalilem4  25932  mbflimsup  25987  itg11  26012  i1faddlem  26014  i1fmullem  26015  itg1mulc  26025  i1fres  26026  itg1climres  26035  mbfi1fseqlem3  26038  itg2seq  26063  itg2monolem2  26072  itg2monolem3  26073  itg2mono  26074  itg2cnlem1  26082  limciun  26214  dvcnvlem  26296  dvivthlem2  26329  dvivth  26330  lhop1lem  26333  lhop1  26334  lhop2  26335  aalioulem3  26661  basellem3  27410  nodenselem8  28048  noseq0  28676  noseqp1  28677  noseqrdg0  28693  tgelrnln  29098  wlkiswwlks1  30456  ubthlem1  31472  pjrni  32304  pjoi0  32319  hmopidmchi  32753  hmopidmpji  32754  pjssdif1i  32777  dfpjop  32784  pjadj3  32790  elpjrn  32792  pjcmul1i  32803  pjcmul2i  32804  pj3si  32809  ofrn2  33234  prodindf  33429  mgcf1o  33564  cycpmfvlem  33673  cycpmfv1  33674  cycpmfv2  33675  locfinreflem  34472  cnre2csqlem  34542  elmrsubrn  36285  elmsubrn  36293  msubrn  36294  elmsta  36313  vhmcls  36331  mclsppslem  36348  neibastop2lem  37148  tailfb  37165  fvineqsneu  38334  ptrecube  38538  heicant  38573  mblfinlem2  38576  ftc1anclem7  38617  ftc1anc  38619  sstotbnd2  38708  prdsbnd  38727  heibor1lem  38743  heiborlem1  38745  dihcl  42327  dih0rn  42341  dih1dimatlem  42386  dihlspsnssN  42389  dochocss  42423  hdmaprnlem17N  42920  hgmaprnlem1N  42953  nacsfix  43722  kercvrlsm  44084  pwssplit4  44090  tfsconcatrev  44349  orbitinit  45945  orbitcl  45946  climinf  46617  climinf2lem  46715  limsupvaluz2  46747  supcnvlimsup  46749  fourierdlem25  47141  fourierdlem42  47158  fourierdlem54  47169  fourierdlem64  47179  fourierdlem65  47180  sge0le  47416  sge0seq  47455  imaelsetpreimafv  48476