Theorem fnfvelrn 6958

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ran crn 5590   Fn wfn 6428  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fn 6436  df-fv 6441

This theorem is referenced by:  ffvelrn  6959  fvcofneq  6969  fnovrn  7447  fo1stres  7857  fo2ndres  7858  offsplitfpar  7960  fo2ndf  7962  seqomlem3  8283  seqomlem4  8284  phplem2  8991  phplem4OLD  9003  indexfi  9127  dffi3  9190  ordtypelem7  9283  inf0  9379  infdifsn  9415  noinfep  9418  cantnflem3  9449  cantnf  9451  cardinfima  9853  alephfplem1  9860  alephfplem3  9862  alephfp  9864  dfac5  9884  dfac12lem2  9900  cfflb  10015  sornom  10033  fin23lem16  10091  fin23lem20  10093  isf32lem2  10110  axcc2lem  10192  axdc3lem2  10207  ttukeylem6  10270  konigthlem  10324  pwcfsdom  10339  pwfseqlem1  10414  gch2  10431  1nn  11984  peano2nn  11985  rpnnen1lem5  12721  om2uzrani  13672  uzrdglem  13677  uzrdg0i  13679  fseqsupubi  13698  ccatrn  14294  uzin2  15056  climsup  15381  ruclem12  15950  0ram  16721  setcepi  17803  acsmapd  18272  cycsubgcl  18825  ghmrn  18847  conjnmz  18868  pmtrrn  19065  sylow1lem4  19206  pgpssslw  19219  sylow2blem3  19227  sylow3lem2  19233  efgsfo  19345  gexex  19454  gsumval3eu  19505  gsumzsplit  19528  pjfo  20922  issubassa2  21096  mplbas2  21243  mpfconst  21311  mpfproj  21312  mpfind  21317  pf1const  21512  pf1id  21513  mpfpf1  21517  pf1mpf  21518  toprntopon  22074  cmpsub  22551  conncn  22577  2ndcctbss  22606  2ndcdisj  22607  2ndcsep  22610  iskgen2  22699  kgen2cn  22710  ptbasfi  22732  ptcnplem  22772  isr0  22888  r0cld  22889  zfbas  23047  uzrest  23048  rnelfm  23104  tmdgsum2  23247  evth  24122  bcth3  24495  ivthicc  24622  ovolmge0  24641  ovollb2lem  24652  ovolunlem1a  24660  ovoliunlem1  24666  ovoliun  24669  ovolicc2lem4  24684  voliunlem1  24714  voliunlem3  24716  volsup  24720  ioombl1lem2  24723  ioombl1lem4  24725  uniioombllem2  24747  uniioombllem3  24749  vitalilem2  24773  vitalilem4  24775  mbflimsup  24830  itg11  24855  i1faddlem  24857  i1fmullem  24858  itg1mulc  24869  i1fres  24870  itg1climres  24879  mbfi1fseqlem3  24882  itg2seq  24907  itg2monolem2  24916  itg2monolem3  24917  itg2mono  24918  itg2cnlem1  24926  limciun  25058  dvcnvlem  25140  dvivthlem2  25173  dvivth  25174  lhop1lem  25177  lhop1  25178  lhop2  25179  aalioulem3  25494  basellem3  26232  tgelrnln  26991  wlkiswwlks1  28232  ubthlem1  29232  pjrni  30064  pjoi0  30079  hmopidmchi  30513  hmopidmpji  30514  pjssdif1i  30537  dfpjop  30544  pjadj3  30550  elpjrn  30552  pjcmul1i  30563  pjcmul2i  30564  pj3si  30569  ofrn2  30977  mgcf1o  31281  cycpmfvlem  31379  cycpmfv1  31380  cycpmfv2  31381  locfinreflem  31790  cnre2csqlem  31860  prodindf  31991  elmrsubrn  33482  elmsubrn  33490  msubrn  33491  elmsta  33510  vhmcls  33528  mclsppslem  33545  nodenselem8  33894  neibastop2lem  34549  tailfb  34566  fvineqsneu  35582  ptrecube  35777  heicant  35812  mblfinlem2  35815  ftc1anclem7  35856  ftc1anc  35858  sstotbnd2  35932  prdsbnd  35951  heibor1lem  35967  heiborlem1  35969  dihcl  39284  dih0rn  39298  dih1dimatlem  39343  dihlspsnssN  39346  dochocss  39380  hdmaprnlem17N  39877  hgmaprnlem1N  39910  nacsfix  40534  kercvrlsm  40908  pwssplit4  40914  ssmapsn  42756  fnfvelrnd  42808  climinf  43147  climinf2lem  43247  limsupvaluz2  43279  supcnvlimsup  43281  fourierdlem25  43673  fourierdlem42  43690  fourierdlem54  43701  fourierdlem64  43711  fourierdlem65  43712  sge0le  43945  sge0seq  43984  imaelsetpreimafv  44847  offvalfv  45678