Theorem fnfvelrn 7114

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ran crn 5701   Fn wfn 6568  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-fv 6581

This theorem is referenced by:  ffvelcdm  7115  fnfvelrnd  7116  fvcofneq  7127  fnovrn  7625  fo1stres  8056  fo2ndres  8057  offsplitfpar  8160  fo2ndf  8162  seqomlem3  8508  seqomlem4  8509  phplem2  9271  phplem4OLD  9283  indexfi  9430  dffi3  9500  ordtypelem7  9593  inf0  9690  infdifsn  9726  noinfep  9729  cantnflem3  9760  cantnf  9762  cardinfima  10166  alephfplem1  10173  alephfplem3  10175  alephfp  10177  dfac5  10198  dfac12lem2  10214  cfflb  10328  sornom  10346  fin23lem16  10404  fin23lem20  10406  isf32lem2  10423  axcc2lem  10505  axdc3lem2  10520  ttukeylem6  10583  konigthlem  10637  pwcfsdom  10652  pwfseqlem1  10727  gch2  10744  1nn  12304  peano2nn  12305  rpnnen1lem5  13046  om2uzrani  14003  uzrdglem  14008  uzrdg0i  14010  fseqsupubi  14029  ccatrn  14637  uzin2  15393  climsup  15718  ruclem12  16289  0ram  17067  setcepi  18155  acsmapd  18624  cycsubgcl  19246  ghmrn  19269  conjnmz  19292  pmtrrn  19499  sylow1lem4  19643  pgpssslw  19656  sylow2blem3  19664  sylow3lem2  19670  efgsfo  19781  gexex  19895  gsumval3eu  19946  gsumzsplit  19969  pjfo  21758  issubassa2  21935  mplbas2  22083  mpfconst  22148  mpfproj  22149  mpfind  22154  pf1const  22371  pf1id  22372  mpfpf1  22376  pf1mpf  22377  toprntopon  22952  cmpsub  23429  conncn  23455  2ndcctbss  23484  2ndcdisj  23485  2ndcsep  23488  iskgen2  23577  kgen2cn  23588  ptbasfi  23610  ptcnplem  23650  isr0  23766  r0cld  23767  zfbas  23925  uzrest  23926  rnelfm  23982  tmdgsum2  24125  evth  25010  bcth3  25384  ivthicc  25512  ovolmge0  25531  ovollb2lem  25542  ovolunlem1a  25550  ovoliunlem1  25556  ovoliun  25559  ovolicc2lem4  25574  voliunlem1  25604  voliunlem3  25606  volsup  25610  ioombl1lem2  25613  ioombl1lem4  25615  uniioombllem2  25637  uniioombllem3  25639  vitalilem2  25663  vitalilem4  25665  mbflimsup  25720  itg11  25745  i1faddlem  25747  i1fmullem  25748  itg1mulc  25759  i1fres  25760  itg1climres  25769  mbfi1fseqlem3  25772  itg2seq  25797  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itg2cnlem1  25816  limciun  25949  dvcnvlem  26034  dvivthlem2  26068  dvivth  26069  lhop1lem  26072  lhop1  26073  lhop2  26074  aalioulem3  26394  basellem3  27144  nodenselem8  27754  noseq0  28314  noseqp1  28315  noseqrdg0  28331  tgelrnln  28656  wlkiswwlks1  29900  ubthlem1  30902  pjrni  31734  pjoi0  31749  hmopidmchi  32183  hmopidmpji  32184  pjssdif1i  32207  dfpjop  32214  pjadj3  32220  elpjrn  32222  pjcmul1i  32233  pjcmul2i  32234  pj3si  32239  ofrn2  32659  mgcf1o  32976  cycpmfvlem  33105  cycpmfv1  33106  cycpmfv2  33107  locfinreflem  33786  cnre2csqlem  33856  prodindf  33987  elmrsubrn  35488  elmsubrn  35496  msubrn  35497  elmsta  35516  vhmcls  35534  mclsppslem  35551  neibastop2lem  36326  tailfb  36343  fvineqsneu  37377  ptrecube  37580  heicant  37615  mblfinlem2  37618  ftc1anclem7  37659  ftc1anc  37661  sstotbnd2  37734  prdsbnd  37753  heibor1lem  37769  heiborlem1  37771  dihcl  41227  dih0rn  41241  dih1dimatlem  41286  dihlspsnssN  41289  dochocss  41323  hdmaprnlem17N  41820  hgmaprnlem1N  41853  nacsfix  42668  kercvrlsm  43040  pwssplit4  43046  tfsconcatrev  43310  ssmapsn  45123  climinf  45527  climinf2lem  45627  limsupvaluz2  45659  supcnvlimsup  45661  fourierdlem25  46053  fourierdlem42  46070  fourierdlem54  46081  fourierdlem64  46091  fourierdlem65  46092  sge0le  46328  sge0seq  46367  imaelsetpreimafv  47269  offvalfv  48067