Theorem fnfvelrn 7032

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ran crn 5632   Fn wfn 6493  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-fv 6506

This theorem is referenced by:  ffvelcdm  7033  fnfvelrnd  7034  fvcofneq  7045  fnovrn  7542  offvalfv  7653  fo1stres  7968  fo2ndres  7969  offsplitfpar  8069  fo2ndf  8071  seqomlem3  8391  seqomlem4  8392  phplem2  9139  indexfi  9270  dffi3  9344  ordtypelem7  9439  inf0  9542  infdifsn  9578  noinfep  9581  cantnflem3  9612  cantnf  9614  cardinfima  10019  alephfplem1  10026  alephfplem3  10028  alephfp  10030  dfac5  10051  dfac12lem2  10067  cfflb  10181  sornom  10199  fin23lem16  10257  fin23lem20  10259  isf32lem2  10276  axcc2lem  10358  axdc3lem2  10373  ttukeylem6  10436  konigthlem  10491  pwcfsdom  10506  pwfseqlem1  10581  gch2  10598  1nn  12185  peano2nn  12186  rpnnen1lem5  12931  om2uzrani  13914  uzrdglem  13919  uzrdg0i  13921  fseqsupubi  13940  ccatrn  14552  uzin2  15307  climsup  15632  ruclem12  16208  0ram  16991  setcepi  18055  acsmapd  18520  cycsubgcl  19181  ghmrn  19204  conjnmz  19227  pmtrrn  19432  sylow1lem4  19576  pgpssslw  19589  sylow2blem3  19597  sylow3lem2  19603  efgsfo  19714  gexex  19828  gsumval3eu  19879  gsumzsplit  19902  pjfo  21695  issubassa2  21872  mplbas2  22020  mpfconst  22087  mpfproj  22088  mpfind  22093  pf1const  22311  pf1id  22312  mpfpf1  22316  pf1mpf  22317  toprntopon  22890  cmpsub  23365  conncn  23391  2ndcctbss  23420  2ndcdisj  23421  2ndcsep  23424  iskgen2  23513  kgen2cn  23524  ptbasfi  23546  ptcnplem  23586  isr0  23702  r0cld  23703  zfbas  23861  uzrest  23862  rnelfm  23918  tmdgsum2  24061  evth  24926  bcth3  25298  ivthicc  25425  ovolmge0  25444  ovollb2lem  25455  ovolunlem1a  25463  ovoliunlem1  25469  ovoliun  25472  ovolicc2lem4  25487  voliunlem1  25517  voliunlem3  25519  volsup  25523  ioombl1lem2  25526  ioombl1lem4  25528  uniioombllem2  25550  uniioombllem3  25552  vitalilem2  25576  vitalilem4  25578  mbflimsup  25633  itg11  25658  i1faddlem  25660  i1fmullem  25661  itg1mulc  25671  i1fres  25672  itg1climres  25681  mbfi1fseqlem3  25684  itg2seq  25709  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2cnlem1  25728  limciun  25861  dvcnvlem  25943  dvivthlem2  25976  dvivth  25977  lhop1lem  25980  lhop1  25981  lhop2  25982  aalioulem3  26300  basellem3  27046  nodenselem8  27655  noseq0  28282  noseqp1  28283  noseqrdg0  28299  tgelrnln  28698  wlkiswwlks1  29935  ubthlem1  30941  pjrni  31773  pjoi0  31788  hmopidmchi  32222  hmopidmpji  32223  pjssdif1i  32246  dfpjop  32253  pjadj3  32259  elpjrn  32261  pjcmul1i  32272  pjcmul2i  32273  pj3si  32278  ofrn2  32713  prodindf  32922  mgcf1o  33063  cycpmfvlem  33173  cycpmfv1  33174  cycpmfv2  33175  locfinreflem  33984  cnre2csqlem  34054  elmrsubrn  35702  elmsubrn  35710  msubrn  35711  elmsta  35730  vhmcls  35748  mclsppslem  35765  neibastop2lem  36542  tailfb  36559  fvineqsneu  37727  ptrecube  37941  heicant  37976  mblfinlem2  37979  ftc1anclem7  38020  ftc1anc  38022  sstotbnd2  38095  prdsbnd  38114  heibor1lem  38130  heiborlem1  38132  dihcl  41716  dih0rn  41730  dih1dimatlem  41775  dihlspsnssN  41778  dochocss  41812  hdmaprnlem17N  42309  hgmaprnlem1N  42342  nacsfix  43144  kercvrlsm  43511  pwssplit4  43517  tfsconcatrev  43776  orbitinit  45383  orbitcl  45384  climinf  46036  climinf2lem  46134  limsupvaluz2  46166  supcnvlimsup  46168  fourierdlem25  46560  fourierdlem42  46577  fourierdlem54  46588  fourierdlem64  46598  fourierdlem65  46599  sge0le  46835  sge0seq  46874  imaelsetpreimafv  47855