Theorem fnfvelrn 7056

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ran crn 5644   Fn wfn 6511  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-iota 6472  df-fun 6518  df-fn 6519  df-fv 6524

This theorem is referenced by:  ffvelcdm  7057  fnfvelrnd  7058  fvcofneq  7069  fnovrn  7566  offvalfv  7677  fo1stres  7991  fo2ndres  7992  offsplitfpar  8092  fo2ndf  8094  seqomlem3  8417  seqomlem4  8418  phplem2  9167  indexfi  9297  dffi3  9371  ordtypelem7  9466  inf0  9570  infdifsn  9606  noinfep  9609  cantnflem3  9640  cantnf  9642  cardinfima  10047  alephfplem1  10054  alephfplem3  10056  alephfp  10058  dfac5  10079  dfac12lem2  10095  cfflb  10210  sornom  10228  fin23lem16  10286  fin23lem20  10288  isf32lem2  10305  axcc2lem  10387  axdc3lem2  10402  ttukeylem6  10465  konigthlem  10520  pwcfsdom  10535  pwfseqlem1  10610  gch2  10627  1nn  12215  peano2nn  12216  rpnnen1lem5  12976  om2uzrani  13959  uzrdglem  13964  uzrdg0i  13966  fseqsupubi  13985  ccatrn  14597  uzin2  15363  climsup  15688  ruclem12  16264  0ram  17047  setcepi  18112  acsmapd  18577  cycsubgcl  19238  ghmrn  19260  conjnmz  19283  pmtrrn  19488  sylow1lem4  19632  pgpssslw  19645  sylow2blem3  19653  sylow3lem2  19659  efgsfo  19770  gexex  19884  gsumval3eu  19935  gsumzsplit  19958  pjfo  21755  issubassa2  21932  mplbas2  22083  mpfconst  22150  mpfproj  22151  mpfind  22156  pf1const  22397  pf1id  22398  mpfpf1  22402  pf1mpf  22403  toprntopon  22973  cmpsub  23448  conncn  23474  2ndcctbss  23503  2ndcdisj  23504  2ndcsep  23507  iskgen2  23596  kgen2cn  23607  ptbasfi  23629  ptcnplem  23669  isr0  23785  r0cld  23786  zfbas  23944  uzrest  23945  rnelfm  24001  tmdgsum2  24144  evth  25009  bcth3  25381  ivthicc  25508  ovolmge0  25527  ovollb2lem  25538  ovolunlem1a  25546  ovoliunlem1  25552  ovoliun  25555  ovolicc2lem4  25570  voliunlem1  25600  voliunlem3  25602  volsup  25606  ioombl1lem2  25609  ioombl1lem4  25611  uniioombllem2  25633  uniioombllem3  25635  vitalilem2  25659  vitalilem4  25661  mbflimsup  25716  itg11  25741  i1faddlem  25743  i1fmullem  25744  itg1mulc  25754  i1fres  25755  itg1climres  25764  mbfi1fseqlem3  25767  itg2seq  25792  itg2monolem2  25801  itg2monolem3  25802  itg2mono  25803  itg2cnlem1  25811  limciun  25944  dvcnvlem  26026  dvivthlem2  26059  dvivth  26060  lhop1lem  26063  lhop1  26064  lhop2  26065  aalioulem3  26386  basellem3  27135  nodenselem8  27743  noseq0  28371  noseqp1  28372  noseqrdg0  28388  tgelrnln  28787  wlkiswwlks1  30024  ubthlem1  31030  pjrni  31862  pjoi0  31877  hmopidmchi  32311  hmopidmpji  32312  pjssdif1i  32335  dfpjop  32342  pjadj3  32348  elpjrn  32350  pjcmul1i  32361  pjcmul2i  32362  pj3si  32367  ofrn2  32803  prodindf  33001  mgcf1o  33142  cycpmfvlem  33253  cycpmfv1  33254  cycpmfv2  33255  locfinreflem  34098  cnre2csqlem  34168  elmrsubrn  35831  elmsubrn  35839  msubrn  35840  elmsta  35859  vhmcls  35877  mclsppslem  35894  neibastop2lem  36681  tailfb  36698  fvineqsneu  37866  ptrecube  38080  heicant  38115  mblfinlem2  38118  ftc1anclem7  38159  ftc1anc  38161  sstotbnd2  38234  prdsbnd  38253  heibor1lem  38269  heiborlem1  38271  dihcl  41855  dih0rn  41869  dih1dimatlem  41914  dihlspsnssN  41917  dochocss  41951  hdmaprnlem17N  42448  hgmaprnlem1N  42481  nacsfix  43254  kercvrlsm  43621  pwssplit4  43627  tfsconcatrev  43886  orbitinit  45493  orbitcl  45494  climinf  46143  climinf2lem  46241  limsupvaluz2  46273  supcnvlimsup  46275  fourierdlem25  46667  fourierdlem42  46684  fourierdlem54  46695  fourierdlem64  46705  fourierdlem65  46706  sge0le  46942  sge0seq  46981  imaelsetpreimafv  47962