Theorem fnfvelrn 6264

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ran crn 5039   Fn wfn 5799  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812

This theorem is referenced by:  ffvelrn  6265  fvcofneq  6275  fnovrn  6707  fo1stres  7083  fo2ndres  7084  fo2ndf  7171  seqomlem3  7434  seqomlem4  7435  phplem4  8027  indexfi  8157  dffi3  8220  ordtypelem7  8312  inf0  8401  infdifsn  8437  noinfep  8440  cantnflem3  8471  cantnf  8473  cardinfima  8803  alephfplem1  8810  alephfplem3  8812  alephfp  8814  dfac5  8834  dfac12lem2  8849  cfflb  8964  sornom  8982  fin23lem16  9040  fin23lem20  9042  isf32lem2  9059  axcc2lem  9141  axdc3lem2  9156  ttukeylem6  9219  konigthlem  9269  pwcfsdom  9284  pwfseqlem1  9359  gch2  9376  1nn  10908  peano2nn  10909  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  om2uzrani  12613  uzrdglem  12618  uzrdg0i  12620  fseqsupubi  12639  ccatrn  13225  uzin2  13932  climsup  14248  ruclem12  14809  0ram  15562  setcepi  16561  acsmapd  17001  cycsubgcl  17443  ghmrn  17496  conjnmz  17517  pmtrrn  17700  sylow1lem4  17839  pgpssslw  17852  sylow2blem3  17860  sylow3lem2  17866  efgsfo  17975  gexex  18079  gsumval3eu  18128  gsumzsplit  18150  issubassa2  19166  mplbas2  19291  mpfconst  19351  mpfproj  19352  mpfind  19357  pf1const  19531  pf1id  19532  mpfpf1  19536  pf1mpf  19537  pjfo  19878  cmpsub  21013  concn  21039  2ndcctbss  21068  2ndcdisj  21069  2ndcsep  21072  iskgen2  21161  kgen2cn  21172  ptbasfi  21194  ptcnplem  21234  isr0  21350  r0cld  21351  zfbas  21510  uzrest  21511  rnelfm  21567  tmdgsum2  21710  evth  22566  bcth3  22936  ivthicc  23034  ovolmge0  23052  ovollb2lem  23063  ovolunlem1a  23071  ovoliunlem1  23077  ovoliun  23080  ovolicc2lem4  23095  voliunlem1  23125  voliunlem3  23127  volsup  23131  ioombl1lem2  23134  ioombl1lem4  23136  uniioombllem2  23157  uniioombllem3  23159  vitalilem2  23184  vitalilem4  23186  mbflimsup  23239  itg11  23264  i1faddlem  23266  i1fmullem  23267  itg1mulc  23277  i1fres  23278  itg1climres  23287  mbfi1fseqlem3  23290  itg2seq  23315  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itg2cnlem1  23334  limciun  23464  dvcnvlem  23543  dvivthlem2  23576  dvivth  23577  lhop1lem  23580  lhop1  23581  lhop2  23582  aalioulem3  23893  basellem3  24609  tgelrnln  25325  ubthlem1  27110  pjrni  27945  pjoi0  27960  hmopidmchi  28394  hmopidmpji  28395  pjssdif1i  28418  dfpjop  28425  pjadj3  28431  elpjrn  28433  pjcmul1i  28444  pjcmul2i  28445  pj3si  28450  ofrn2  28822  locfinreflem  29235  cnre2csqlem  29284  elmrsubrn  30671  elmsubrn  30679  msubrn  30680  elmsta  30699  vhmcls  30717  mclsppslem  30734  nodenselem8  31087  neibastop2lem  31525  tailfb  31542  bj-toprntopon  32244  ptrecube  32579  heicant  32614  mblfinlem2  32617  ftc1anclem7  32661  ftc1anc  32663  sstotbnd2  32743  prdsbnd  32762  heibor1lem  32778  heiborlem1  32780  dihcl  35577  dih0rn  35591  dih1dimatlem  35636  dihlspsnssN  35639  dochocss  35673  hdmaprnlem17N  36173  hgmaprnlem1N  36206  nacsfix  36293  kercvrlsm  36671  pwssplit4  36677  ssmapsn  38403  climinf  38673  fourierdlem25  39025  fourierdlem42  39042  fourierdlem54  39053  fourierdlem64  39063  fourierdlem65  39064  sge0le  39300  sge0seq  39339  1wlkiswwlks1  41064  offvalfv  41914