Theorem fnfvelrn 7079

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ran crn 5664   Fn wfn 6535  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is used by:  ffvelcdm  7080  fnfvelrnd  7081  fvcofneq  7092  fnovrn  7595  offvalfv  7706  fo1stres  8018  fo2ndres  8019  offsplitfpar  8120  fo2ndf  8122  seqomlem3  8445  seqomlem4  8446  phplem2  9196  indexfi  9324  dffi3  9398  ordtypelem7  9493  inf0  9597  infdifsn  9633  noinfep  9636  cantnflem3  9667  cantnf  9669  cardinfima  10097  alephfplem1  10104  alephfplem3  10106  alephfp  10108  dfac5  10128  dfac12lem2  10144  cfflb  10258  sornom  10276  fin23lem16  10334  fin23lem20  10336  isf32lem2  10353  axcc2lem  10435  axdc3lem2  10450  ttukeylem6  10513  konigthlem  10568  pwcfsdom  10583  pwfseqlem1  10658  gch2  10675  1nn  12259  peano2nn  12260  rpnnen1lem5  13021  om2uzrani  14006  uzrdglem  14011  uzrdg0i  14013  fseqsupubi  14032  ccatrn  14645  sgnrn  15159  uzin2  15420  climsup  15745  ruclem12  16319  0ram  17102  setcepi  18167  acsmapd  18632  cycsubgcl  19321  ghmrn  19343  conjnmz  19366  pmtrrn  19571  sylow1lem4  19715  pgpssslw  19728  sylow2blem3  19736  sylow3lem2  19742  efgsfo  19853  gexex  19967  gsumval3eu  20018  gsumzsplit  20041  pjfo  21915  issubassa2  22092  mplbas2  22243  mpfconst  22310  mpfproj  22311  mpfind  22316  pf1const  22556  pf1id  22557  mpfpf1  22561  pf1mpf  22562  toprntopon  23132  cmpsub  23607  conncn  23633  2ndcctbss  23663  2ndcdisj  23664  2ndcsep  23667  iskgen2  23756  kgen2cn  23767  ptbasfi  23789  ptcnplem  23829  isr0  23945  r0cld  23946  zfbas  24104  uzrest  24105  rnelfm  24161  tmdgsum2  24304  evth  25169  bcth3  25541  ivthicc  25668  ovolmge0  25687  ovollb2lem  25698  ovolunlem1a  25706  ovoliunlem1  25712  ovoliun  25715  ovolicc2lem4  25730  voliunlem1  25760  voliunlem3  25762  volsup  25766  ioombl1lem2  25769  ioombl1lem4  25771  uniioombllem2  25793  uniioombllem3  25795  vitalilem2  25819  vitalilem4  25821  mbflimsup  25876  itg11  25901  i1faddlem  25903  i1fmullem  25904  itg1mulc  25914  i1fres  25915  itg1climres  25924  mbfi1fseqlem3  25927  itg2seq  25952  itg2monolem2  25961  itg2monolem3  25962  itg2mono  25963  itg2cnlem1  25971  limciun  26104  dvcnvlem  26186  dvivthlem2  26219  dvivth  26220  lhop1lem  26223  lhop1  26224  lhop2  26225  aalioulem3  26548  basellem3  27298  nodenselem8  27906  noseq0  28534  noseqp1  28535  noseqrdg0  28551  tgelrnln  28954  wlkiswwlks1  30283  ubthlem1  31293  pjrni  32125  pjoi0  32140  hmopidmchi  32574  hmopidmpji  32575  pjssdif1i  32598  dfpjop  32605  pjadj3  32611  elpjrn  32613  pjcmul1i  32624  pjcmul2i  32625  pj3si  32630  ofrn2  33056  prodindf  33252  mgcf1o  33387  cycpmfvlem  33496  cycpmfv1  33497  cycpmfv2  33498  locfinreflem  34294  cnre2csqlem  34364  elmrsubrn  36049  elmsubrn  36057  msubrn  36058  elmsta  36077  vhmcls  36095  mclsppslem  36112  neibastop2lem  36928  tailfb  36945  fvineqsneu  38114  ptrecube  38328  heicant  38363  mblfinlem2  38366  ftc1anclem7  38407  ftc1anc  38409  sstotbnd2  38483  prdsbnd  38502  heibor1lem  38518  heiborlem1  38520  dihcl  42102  dih0rn  42116  dih1dimatlem  42161  dihlspsnssN  42164  dochocss  42198  hdmaprnlem17N  42695  hgmaprnlem1N  42728  nacsfix  43501  kercvrlsm  43868  pwssplit4  43874  tfsconcatrev  44133  orbitinit  45723  orbitcl  45724  climinf  46380  climinf2lem  46478  limsupvaluz2  46510  supcnvlimsup  46512  fourierdlem25  46904  fourierdlem42  46921  fourierdlem54  46932  fourierdlem64  46942  fourierdlem65  46943  sge0le  47179  sge0seq  47218  imaelsetpreimafv  48202