Theorem fnfvelrn 7083

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ran crn 5651   Fn wfn 6536  ‘cfv 6541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6496  df-fun 6543  df-fn 6544  df-fv 6549

This theorem is used by:  ffvelcdm  7084  fnfvelrnd  7085  fvcofneq  7096  fnovrn  7598  offvalfv  7717  fo1stres  8029  fo2ndres  8030  offsplitfpar  8134  fo2ndf  8136  seqomlem3  8467  seqomlem4  8468  phplem2  9225  indexfi  9354  dffi3  9428  ordtypelem7  9523  inf0  9627  infdifsn  9663  noinfep  9666  cantnflem3  9697  cantnf  9699  cardinfima  10181  alephfplem1  10188  alephfplem3  10190  alephfp  10192  dfac5  10212  dfac12lem2  10228  cfflb  10342  sornom  10360  fin23lem16  10418  fin23lem20  10420  isf32lem2  10437  axcc2lem  10519  axdc3lem2  10534  ttukeylem6  10597  konigthlem  10658  pwcfsdom  10673  pwfseqlem1  10748  gch2  10765  1nn  12351  peano2nn  12352  rpnnen1lem5  13114  om2uzrani  14100  uzrdglem  14105  uzrdg0i  14107  fseqsupubi  14126  ccatrn  14740  sgnrn  15258  uzin2  15519  climsup  15844  ruclem12  16416  0ram  17205  setcepi  18270  acsmapd  18735  cycsubgcl  19428  ghmrn  19450  conjnmz  19473  pmtrrn  19678  sylow1lem4  19822  pgpssslw  19835  sylow2blem3  19843  sylow3lem2  19849  efgsfo  19960  gexex  20074  gsumval3eu  20125  gsumzsplit  20148  pjfo  22028  issubassa2  22207  mplbas2  22358  mpfconst  22425  mpfproj  22426  mpfind  22431  pf1const  22671  pf1id  22672  mpfpf1  22676  pf1mpf  22677  toprntopon  23250  cmpsub  23725  conncn  23751  2ndcctbss  23781  2ndcdisj  23782  2ndcsep  23785  iskgen2  23874  kgen2cn  23885  ptbasfi  23907  ptcnplem  23947  isr0  24063  r0cld  24064  zfbas  24222  uzrest  24223  rnelfm  24279  tmdgsum2  24422  evth  25287  bcth3  25659  ivthicc  25786  ovolmge0  25805  ovollb2lem  25816  ovolunlem1a  25824  ovoliunlem1  25830  ovoliun  25833  ovolicc2lem4  25848  voliunlem1  25878  voliunlem3  25880  volsup  25884  ioombl1lem2  25887  ioombl1lem4  25889  uniioombllem2  25911  uniioombllem3  25913  vitalilem2  25937  vitalilem4  25939  mbflimsup  25994  itg11  26019  i1faddlem  26021  i1fmullem  26022  itg1mulc  26032  i1fres  26033  itg1climres  26042  mbfi1fseqlem3  26045  itg2seq  26070  itg2monolem2  26079  itg2monolem3  26080  itg2mono  26081  itg2cnlem1  26089  limciun  26221  dvcnvlem  26303  dvivthlem2  26336  dvivth  26337  lhop1lem  26340  lhop1  26341  lhop2  26342  aalioulem3  26668  basellem3  27417  nodenselem8  28055  noseq0  28683  noseqp1  28684  noseqrdg0  28700  tgelrnln  29105  wlkiswwlks1  30463  ubthlem1  31479  pjrni  32311  pjoi0  32326  hmopidmchi  32760  hmopidmpji  32761  pjssdif1i  32784  dfpjop  32791  pjadj3  32797  elpjrn  32799  pjcmul1i  32810  pjcmul2i  32811  pj3si  32816  ofrn2  33283  prodindf  33477  mgcf1o  33612  cycpmfvlem  33721  cycpmfv1  33722  cycpmfv2  33723  locfinreflem  34520  cnre2csqlem  34590  elmrsubrn  36373  elmsubrn  36381  msubrn  36382  elmsta  36401  vhmcls  36419  mclsppslem  36436  neibastop2lem  37242  tailfb  37259  fvineqsneu  38441  ptrecube  38645  heicant  38680  mblfinlem2  38683  ftc1anclem7  38724  ftc1anc  38726  sstotbnd2  38815  prdsbnd  38834  heibor1lem  38850  heiborlem1  38852  dihcl  42434  dih0rn  42448  dih1dimatlem  42493  dihlspsnssN  42496  dochocss  42530  hdmaprnlem17N  43027  hgmaprnlem1N  43060  nacsfix  43830  kercvrlsm  44192  pwssplit4  44198  tfsconcatrev  44457  orbitinit  46053  orbitcl  46054  climinf  46725  climinf2lem  46823  limsupvaluz2  46855  supcnvlimsup  46857  fourierdlem25  47249  fourierdlem42  47266  fourierdlem54  47277  fourierdlem64  47287  fourierdlem65  47288  sge0le  47524  sge0seq  47563  imaelsetpreimafv  48584