Theorem fnfvelrn 7075

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ran crn 5662   Fn wfn 6531  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  ffvelcdm  7076  fnfvelrnd  7077  fvcofneq  7088  fnovrn  7585  offvalfv  7696  fo1stres  8008  fo2ndres  8009  offsplitfpar  8110  fo2ndf  8112  seqomlem3  8435  seqomlem4  8436  phplem2  9185  indexfi  9313  dffi3  9387  ordtypelem7  9482  inf0  9586  infdifsn  9622  noinfep  9625  cantnflem3  9656  cantnf  9658  cardinfima  10077  alephfplem1  10084  alephfplem3  10086  alephfp  10088  dfac5  10108  dfac12lem2  10124  cfflb  10238  sornom  10256  fin23lem16  10314  fin23lem20  10316  isf32lem2  10333  axcc2lem  10415  axdc3lem2  10430  ttukeylem6  10493  konigthlem  10548  pwcfsdom  10563  pwfseqlem1  10638  gch2  10655  1nn  12239  peano2nn  12240  rpnnen1lem5  13000  om2uzrani  13984  uzrdglem  13989  uzrdg0i  13991  fseqsupubi  14010  ccatrn  14623  sgnrn  15131  uzin2  15392  climsup  15717  ruclem12  16292  0ram  17075  setcepi  18140  acsmapd  18605  cycsubgcl  19272  ghmrn  19294  conjnmz  19317  pmtrrn  19522  sylow1lem4  19666  pgpssslw  19679  sylow2blem3  19687  sylow3lem2  19693  efgsfo  19804  gexex  19918  gsumval3eu  19969  gsumzsplit  19992  pjfo  21865  issubassa2  22042  mplbas2  22193  mpfconst  22260  mpfproj  22261  mpfind  22266  pf1const  22506  pf1id  22507  mpfpf1  22511  pf1mpf  22512  toprntopon  23082  cmpsub  23557  conncn  23583  2ndcctbss  23612  2ndcdisj  23613  2ndcsep  23616  iskgen2  23705  kgen2cn  23716  ptbasfi  23738  ptcnplem  23778  isr0  23894  r0cld  23895  zfbas  24053  uzrest  24054  rnelfm  24110  tmdgsum2  24253  evth  25118  bcth3  25490  ivthicc  25617  ovolmge0  25636  ovollb2lem  25647  ovolunlem1a  25655  ovoliunlem1  25661  ovoliun  25664  ovolicc2lem4  25679  voliunlem1  25709  voliunlem3  25711  volsup  25715  ioombl1lem2  25718  ioombl1lem4  25720  uniioombllem2  25742  uniioombllem3  25744  vitalilem2  25768  vitalilem4  25770  mbflimsup  25825  itg11  25850  i1faddlem  25852  i1fmullem  25853  itg1mulc  25863  i1fres  25864  itg1climres  25873  mbfi1fseqlem3  25876  itg2seq  25901  itg2monolem2  25910  itg2monolem3  25911  itg2mono  25912  itg2cnlem1  25920  limciun  26053  dvcnvlem  26135  dvivthlem2  26168  dvivth  26169  lhop1lem  26172  lhop1  26173  lhop2  26174  aalioulem3  26497  basellem3  27247  nodenselem8  27855  noseq0  28483  noseqp1  28484  noseqrdg0  28500  tgelrnln  28903  wlkiswwlks1  30216  ubthlem1  31222  pjrni  32054  pjoi0  32069  hmopidmchi  32503  hmopidmpji  32504  pjssdif1i  32527  dfpjop  32534  pjadj3  32540  elpjrn  32542  pjcmul1i  32553  pjcmul2i  32554  pj3si  32559  ofrn2  32985  prodindf  33182  mgcf1o  33323  cycpmfvlem  33432  cycpmfv1  33433  cycpmfv2  33434  locfinreflem  34230  cnre2csqlem  34300  elmrsubrn  36012  elmsubrn  36020  msubrn  36021  elmsta  36040  vhmcls  36058  mclsppslem  36075  neibastop2lem  36871  tailfb  36888  fvineqsneu  38057  ptrecube  38271  heicant  38306  mblfinlem2  38309  ftc1anclem7  38350  ftc1anc  38352  sstotbnd2  38425  prdsbnd  38444  heibor1lem  38460  heiborlem1  38462  dihcl  42044  dih0rn  42058  dih1dimatlem  42103  dihlspsnssN  42106  dochocss  42140  hdmaprnlem17N  42637  hgmaprnlem1N  42670  nacsfix  43443  kercvrlsm  43810  pwssplit4  43816  tfsconcatrev  44075  orbitinit  45665  orbitcl  45666  climinf  46322  climinf2lem  46420  limsupvaluz2  46452  supcnvlimsup  46454  fourierdlem25  46846  fourierdlem42  46863  fourierdlem54  46874  fourierdlem64  46884  fourierdlem65  46885  sge0le  47121  sge0seq  47160  imaelsetpreimafv  48144