Theorem fnfvelrn 7067

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ran crn 5653   Fn wfn 6523  ‘cfv 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pr 5400

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-id 5546  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6530  df-fn 6531  df-fv 6536

This theorem is referenced by:  ffvelcdm  7068  fnfvelrnd  7069  fvcofneq  7080  fnovrn  7577  offvalfv  7688  fo1stres  8009  fo2ndres  8010  offsplitfpar  8113  fo2ndf  8115  seqomlem3  8461  seqomlem4  8462  phplem2  9214  indexfi  9367  dffi3  9438  ordtypelem7  9531  inf0  9628  infdifsn  9664  noinfep  9667  cantnflem3  9698  cantnf  9700  cardinfima  10104  alephfplem1  10111  alephfplem3  10113  alephfp  10115  dfac5  10136  dfac12lem2  10152  cfflb  10266  sornom  10284  fin23lem16  10342  fin23lem20  10344  isf32lem2  10361  axcc2lem  10443  axdc3lem2  10458  ttukeylem6  10521  konigthlem  10575  pwcfsdom  10590  pwfseqlem1  10665  gch2  10682  1nn  12244  peano2nn  12245  rpnnen1lem5  12990  om2uzrani  13960  uzrdglem  13965  uzrdg0i  13967  fseqsupubi  13986  ccatrn  14596  uzin2  15352  climsup  15675  ruclem12  16246  0ram  17027  setcepi  18088  acsmapd  18551  cycsubgcl  19176  ghmrn  19199  conjnmz  19222  pmtrrn  19425  sylow1lem4  19569  pgpssslw  19582  sylow2blem3  19590  sylow3lem2  19596  efgsfo  19707  gexex  19821  gsumval3eu  19872  gsumzsplit  19895  pjfo  21662  issubassa2  21839  mplbas2  21987  mpfconst  22046  mpfproj  22047  mpfind  22052  pf1const  22271  pf1id  22272  mpfpf1  22276  pf1mpf  22277  toprntopon  22850  cmpsub  23325  conncn  23351  2ndcctbss  23380  2ndcdisj  23381  2ndcsep  23384  iskgen2  23473  kgen2cn  23484  ptbasfi  23506  ptcnplem  23546  isr0  23662  r0cld  23663  zfbas  23821  uzrest  23822  rnelfm  23878  tmdgsum2  24021  evth  24896  bcth3  25270  ivthicc  25398  ovolmge0  25417  ovollb2lem  25428  ovolunlem1a  25436  ovoliunlem1  25442  ovoliun  25445  ovolicc2lem4  25460  voliunlem1  25490  voliunlem3  25492  volsup  25496  ioombl1lem2  25499  ioombl1lem4  25501  uniioombllem2  25523  uniioombllem3  25525  vitalilem2  25549  vitalilem4  25551  mbflimsup  25606  itg11  25631  i1faddlem  25633  i1fmullem  25634  itg1mulc  25644  i1fres  25645  itg1climres  25654  mbfi1fseqlem3  25657  itg2seq  25682  itg2monolem2  25691  itg2monolem3  25692  itg2mono  25693  itg2cnlem1  25701  limciun  25834  dvcnvlem  25919  dvivthlem2  25953  dvivth  25954  lhop1lem  25957  lhop1  25958  lhop2  25959  aalioulem3  26281  basellem3  27031  nodenselem8  27641  noseq0  28201  noseqp1  28202  noseqrdg0  28218  tgelrnln  28543  wlkiswwlks1  29783  ubthlem1  30785  pjrni  31617  pjoi0  31632  hmopidmchi  32066  hmopidmpji  32067  pjssdif1i  32090  dfpjop  32097  pjadj3  32103  elpjrn  32105  pjcmul1i  32116  pjcmul2i  32117  pj3si  32122  ofrn2  32552  prodindf  32777  mgcf1o  32921  cycpmfvlem  33060  cycpmfv1  33061  cycpmfv2  33062  locfinreflem  33800  cnre2csqlem  33870  elmrsubrn  35471  elmsubrn  35479  msubrn  35480  elmsta  35499  vhmcls  35517  mclsppslem  35534  neibastop2lem  36307  tailfb  36324  fvineqsneu  37358  ptrecube  37573  heicant  37608  mblfinlem2  37611  ftc1anclem7  37652  ftc1anc  37654  sstotbnd2  37727  prdsbnd  37746  heibor1lem  37762  heiborlem1  37764  dihcl  41218  dih0rn  41232  dih1dimatlem  41277  dihlspsnssN  41280  dochocss  41314  hdmaprnlem17N  41811  hgmaprnlem1N  41844  nacsfix  42667  kercvrlsm  43039  pwssplit4  43045  tfsconcatrev  43304  orbitinit  44915  orbitcl  44916  climinf  45571  climinf2lem  45671  limsupvaluz2  45703  supcnvlimsup  45705  fourierdlem25  46097  fourierdlem42  46114  fourierdlem54  46125  fourierdlem64  46135  fourierdlem65  46136  sge0le  46372  sge0seq  46411  imaelsetpreimafv  47335