Theorem fnfvelrn 7073

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

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

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 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-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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  ffvelcdm  7074  fnfvelrnd  7075  fvcofneq  7086  fnovrn  7589  offvalfv  7700  fo1stres  8012  fo2ndres  8013  offsplitfpar  8116  fo2ndf  8118  seqomlem3  8441  seqomlem4  8442  phplem2  9199  indexfi  9327  dffi3  9401  ordtypelem7  9496  inf0  9600  infdifsn  9636  noinfep  9639  cantnflem3  9670  cantnf  9672  cardinfima  10100  alephfplem1  10107  alephfplem3  10109  alephfp  10111  dfac5  10131  dfac12lem2  10147  cfflb  10261  sornom  10279  fin23lem16  10337  fin23lem20  10339  isf32lem2  10356  axcc2lem  10438  axdc3lem2  10453  ttukeylem6  10516  konigthlem  10577  pwcfsdom  10592  pwfseqlem1  10667  gch2  10684  1nn  12268  peano2nn  12269  rpnnen1lem5  13031  om2uzrani  14016  uzrdglem  14021  uzrdg0i  14023  fseqsupubi  14042  ccatrn  14655  sgnrn  15171  uzin2  15432  climsup  15757  ruclem12  16329  0ram  17112  setcepi  18177  acsmapd  18642  cycsubgcl  19334  ghmrn  19356  conjnmz  19379  pmtrrn  19584  sylow1lem4  19728  pgpssslw  19741  sylow2blem3  19749  sylow3lem2  19755  efgsfo  19866  gexex  19980  gsumval3eu  20031  gsumzsplit  20054  pjfo  21928  issubassa2  22107  mplbas2  22258  mpfconst  22325  mpfproj  22326  mpfind  22331  pf1const  22571  pf1id  22572  mpfpf1  22576  pf1mpf  22577  toprntopon  23150  cmpsub  23625  conncn  23651  2ndcctbss  23681  2ndcdisj  23682  2ndcsep  23685  iskgen2  23774  kgen2cn  23785  ptbasfi  23807  ptcnplem  23847  isr0  23963  r0cld  23964  zfbas  24122  uzrest  24123  rnelfm  24179  tmdgsum2  24322  evth  25187  bcth3  25559  ivthicc  25686  ovolmge0  25705  ovollb2lem  25716  ovolunlem1a  25724  ovoliunlem1  25730  ovoliun  25733  ovolicc2lem4  25748  voliunlem1  25778  voliunlem3  25780  volsup  25784  ioombl1lem2  25787  ioombl1lem4  25789  uniioombllem2  25811  uniioombllem3  25813  vitalilem2  25837  vitalilem4  25839  mbflimsup  25894  itg11  25919  i1faddlem  25921  i1fmullem  25922  itg1mulc  25932  i1fres  25933  itg1climres  25942  mbfi1fseqlem3  25945  itg2seq  25970  itg2monolem2  25979  itg2monolem3  25980  itg2mono  25981  itg2cnlem1  25989  limciun  26121  dvcnvlem  26203  dvivthlem2  26236  dvivth  26237  lhop1lem  26240  lhop1  26241  lhop2  26242  aalioulem3  26570  basellem3  27319  nodenselem8  27927  noseq0  28555  noseqp1  28556  noseqrdg0  28572  tgelrnln  28977  wlkiswwlks1  30335  ubthlem1  31351  pjrni  32183  pjoi0  32198  hmopidmchi  32632  hmopidmpji  32633  pjssdif1i  32656  dfpjop  32663  pjadj3  32669  elpjrn  32671  pjcmul1i  32682  pjcmul2i  32683  pj3si  32688  ofrn2  33113  prodindf  33308  mgcf1o  33443  cycpmfvlem  33552  cycpmfv1  33553  cycpmfv2  33554  locfinreflem  34350  cnre2csqlem  34420  elmrsubrn  36099  elmsubrn  36107  msubrn  36108  elmsta  36127  vhmcls  36145  mclsppslem  36162  neibastop2lem  36979  tailfb  36996  fvineqsneu  38165  ptrecube  38369  heicant  38404  mblfinlem2  38407  ftc1anclem7  38448  ftc1anc  38450  sstotbnd2  38524  prdsbnd  38543  heibor1lem  38559  heiborlem1  38561  dihcl  42143  dih0rn  42157  dih1dimatlem  42202  dihlspsnssN  42205  dochocss  42239  hdmaprnlem17N  42736  hgmaprnlem1N  42769  nacsfix  43557  kercvrlsm  43924  pwssplit4  43930  tfsconcatrev  44189  orbitinit  45779  orbitcl  45780  climinf  46436  climinf2lem  46534  limsupvaluz2  46566  supcnvlimsup  46568  fourierdlem25  46960  fourierdlem42  46977  fourierdlem54  46988  fourierdlem64  46998  fourierdlem65  46999  sge0le  47235  sge0seq  47274  imaelsetpreimafv  48295