Theorem fnfvelrn 7078

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ran crn 5652   Fn wfn 6532  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is used by:  ffvelcdm  7079  fnfvelrnd  7080  fvcofneq  7091  fnovrn  7594  offvalfv  7713  fo1stres  8025  fo2ndres  8026  offsplitfpar  8128  fo2ndf  8130  seqomlem3  8455  seqomlem4  8456  phplem2  9213  indexfi  9342  dffi3  9416  ordtypelem7  9511  inf0  9615  infdifsn  9651  noinfep  9654  cantnflem3  9685  cantnf  9687  cardinfima  10169  alephfplem1  10176  alephfplem3  10178  alephfp  10180  dfac5  10200  dfac12lem2  10216  cfflb  10330  sornom  10348  fin23lem16  10406  fin23lem20  10408  isf32lem2  10425  axcc2lem  10507  axdc3lem2  10522  ttukeylem6  10585  konigthlem  10646  pwcfsdom  10661  pwfseqlem1  10736  gch2  10753  1nn  12339  peano2nn  12340  rpnnen1lem5  13102  om2uzrani  14088  uzrdglem  14093  uzrdg0i  14095  fseqsupubi  14114  ccatrn  14728  sgnrn  15244  uzin2  15505  climsup  15830  ruclem12  16402  0ram  17191  setcepi  18256  acsmapd  18721  cycsubgcl  19414  ghmrn  19436  conjnmz  19459  pmtrrn  19664  sylow1lem4  19808  pgpssslw  19821  sylow2blem3  19829  sylow3lem2  19835  efgsfo  19946  gexex  20060  gsumval3eu  20111  gsumzsplit  20134  pjfo  22014  issubassa2  22193  mplbas2  22344  mpfconst  22411  mpfproj  22412  mpfind  22417  pf1const  22657  pf1id  22658  mpfpf1  22662  pf1mpf  22663  toprntopon  23236  cmpsub  23711  conncn  23737  2ndcctbss  23767  2ndcdisj  23768  2ndcsep  23771  iskgen2  23860  kgen2cn  23871  ptbasfi  23893  ptcnplem  23933  isr0  24049  r0cld  24050  zfbas  24208  uzrest  24209  rnelfm  24265  tmdgsum2  24408  evth  25273  bcth3  25645  ivthicc  25772  ovolmge0  25791  ovollb2lem  25802  ovolunlem1a  25810  ovoliunlem1  25816  ovoliun  25819  ovolicc2lem4  25834  voliunlem1  25864  voliunlem3  25866  volsup  25870  ioombl1lem2  25873  ioombl1lem4  25875  uniioombllem2  25897  uniioombllem3  25899  vitalilem2  25923  vitalilem4  25925  mbflimsup  25980  itg11  26005  i1faddlem  26007  i1fmullem  26008  itg1mulc  26018  i1fres  26019  itg1climres  26028  mbfi1fseqlem3  26031  itg2seq  26056  itg2monolem2  26065  itg2monolem3  26066  itg2mono  26067  itg2cnlem1  26075  limciun  26207  dvcnvlem  26289  dvivthlem2  26322  dvivth  26323  lhop1lem  26326  lhop1  26327  lhop2  26328  aalioulem3  26654  basellem3  27403  nodenselem8  28041  noseq0  28669  noseqp1  28670  noseqrdg0  28686  tgelrnln  29091  wlkiswwlks1  30449  ubthlem1  31465  pjrni  32297  pjoi0  32312  hmopidmchi  32746  hmopidmpji  32747  pjssdif1i  32770  dfpjop  32777  pjadj3  32783  elpjrn  32785  pjcmul1i  32796  pjcmul2i  32797  pj3si  32802  ofrn2  33227  prodindf  33422  mgcf1o  33557  cycpmfvlem  33666  cycpmfv1  33667  cycpmfv2  33668  locfinreflem  34465  cnre2csqlem  34535  elmrsubrn  36264  elmsubrn  36272  msubrn  36273  elmsta  36292  vhmcls  36310  mclsppslem  36327  neibastop2lem  37128  tailfb  37145  fvineqsneu  38314  ptrecube  38518  heicant  38553  mblfinlem2  38556  ftc1anclem7  38597  ftc1anc  38599  sstotbnd2  38688  prdsbnd  38707  heibor1lem  38723  heiborlem1  38725  dihcl  42307  dih0rn  42321  dih1dimatlem  42366  dihlspsnssN  42369  dochocss  42403  hdmaprnlem17N  42900  hgmaprnlem1N  42933  nacsfix  43702  kercvrlsm  44069  pwssplit4  44075  tfsconcatrev  44334  orbitinit  45924  orbitcl  45925  climinf  46587  climinf2lem  46685  limsupvaluz2  46717  supcnvlimsup  46719  fourierdlem25  47111  fourierdlem42  47128  fourierdlem54  47139  fourierdlem64  47149  fourierdlem65  47150  sge0le  47386  sge0seq  47425  imaelsetpreimafv  48446