Theorem fnfvelrn 6879

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  ran crn 5537   Fn wfn 6353  ‘cfv 6358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-iota 6316  df-fun 6360  df-fn 6361  df-fv 6366

This theorem is referenced by:  ffvelrn  6880  fvcofneq  6890  fnovrn  7361  fo1stres  7765  fo2ndres  7766  offsplitfpar  7866  fo2ndf  7868  seqomlem3  8166  seqomlem4  8167  phplem4  8806  indexfi  8962  dffi3  9025  ordtypelem7  9118  inf0  9214  infdifsn  9250  noinfep  9253  cantnflem3  9284  cantnf  9286  cardinfima  9676  alephfplem1  9683  alephfplem3  9685  alephfp  9687  dfac5  9707  dfac12lem2  9723  cfflb  9838  sornom  9856  fin23lem16  9914  fin23lem20  9916  isf32lem2  9933  axcc2lem  10015  axdc3lem2  10030  ttukeylem6  10093  konigthlem  10147  pwcfsdom  10162  pwfseqlem1  10237  gch2  10254  1nn  11806  peano2nn  11807  rpnnen1lem5  12542  om2uzrani  13490  uzrdglem  13495  uzrdg0i  13497  fseqsupubi  13516  ccatrn  14111  uzin2  14873  climsup  15198  ruclem12  15765  0ram  16536  setcepi  17548  acsmapd  18014  cycsubgcl  18567  ghmrn  18589  conjnmz  18610  pmtrrn  18803  sylow1lem4  18944  pgpssslw  18957  sylow2blem3  18965  sylow3lem2  18971  efgsfo  19083  gexex  19192  gsumval3eu  19243  gsumzsplit  19266  pjfo  20631  issubassa2  20806  mplbas2  20953  mpfconst  21015  mpfproj  21016  mpfind  21021  pf1const  21216  pf1id  21217  mpfpf1  21221  pf1mpf  21222  toprntopon  21776  cmpsub  22251  conncn  22277  2ndcctbss  22306  2ndcdisj  22307  2ndcsep  22310  iskgen2  22399  kgen2cn  22410  ptbasfi  22432  ptcnplem  22472  isr0  22588  r0cld  22589  zfbas  22747  uzrest  22748  rnelfm  22804  tmdgsum2  22947  evth  23810  bcth3  24182  ivthicc  24309  ovolmge0  24328  ovollb2lem  24339  ovolunlem1a  24347  ovoliunlem1  24353  ovoliun  24356  ovolicc2lem4  24371  voliunlem1  24401  voliunlem3  24403  volsup  24407  ioombl1lem2  24410  ioombl1lem4  24412  uniioombllem2  24434  uniioombllem3  24436  vitalilem2  24460  vitalilem4  24462  mbflimsup  24517  itg11  24542  i1faddlem  24544  i1fmullem  24545  itg1mulc  24556  i1fres  24557  itg1climres  24566  mbfi1fseqlem3  24569  itg2seq  24594  itg2monolem2  24603  itg2monolem3  24604  itg2mono  24605  itg2cnlem1  24613  limciun  24745  dvcnvlem  24827  dvivthlem2  24860  dvivth  24861  lhop1lem  24864  lhop1  24865  lhop2  24866  aalioulem3  25181  basellem3  25919  tgelrnln  26675  wlkiswwlks1  27905  ubthlem1  28905  pjrni  29737  pjoi0  29752  hmopidmchi  30186  hmopidmpji  30187  pjssdif1i  30210  dfpjop  30217  pjadj3  30223  elpjrn  30225  pjcmul1i  30236  pjcmul2i  30237  pj3si  30242  ofrn2  30650  mgcf1o  30954  cycpmfvlem  31052  cycpmfv1  31053  cycpmfv2  31054  locfinreflem  31458  cnre2csqlem  31528  prodindf  31657  elmrsubrn  33149  elmsubrn  33157  msubrn  33158  elmsta  33177  vhmcls  33195  mclsppslem  33212  nodenselem8  33580  neibastop2lem  34235  tailfb  34252  fvineqsneu  35268  ptrecube  35463  heicant  35498  mblfinlem2  35501  ftc1anclem7  35542  ftc1anc  35544  sstotbnd2  35618  prdsbnd  35637  heibor1lem  35653  heiborlem1  35655  dihcl  38970  dih0rn  38984  dih1dimatlem  39029  dihlspsnssN  39032  dochocss  39066  hdmaprnlem17N  39563  hgmaprnlem1N  39596  nacsfix  40178  kercvrlsm  40552  pwssplit4  40558  ssmapsn  42370  fnfvelrnd  42421  climinf  42765  climinf2lem  42865  limsupvaluz2  42897  supcnvlimsup  42899  fourierdlem25  43291  fourierdlem42  43308  fourierdlem54  43319  fourierdlem64  43329  fourierdlem65  43330  sge0le  43563  sge0seq  43602  imaelsetpreimafv  44463  offvalfv  45294