Theorem fnfvelrn 7055

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5642   Fn wfn 6509  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522

This theorem is referenced by:  ffvelcdm  7056  fnfvelrnd  7057  fvcofneq  7068  fnovrn  7567  offvalfv  7678  fo1stres  7997  fo2ndres  7998  offsplitfpar  8101  fo2ndf  8103  seqomlem3  8423  seqomlem4  8424  phplem2  9175  indexfi  9318  dffi3  9389  ordtypelem7  9484  inf0  9581  infdifsn  9617  noinfep  9620  cantnflem3  9651  cantnf  9653  cardinfima  10057  alephfplem1  10064  alephfplem3  10066  alephfp  10068  dfac5  10089  dfac12lem2  10105  cfflb  10219  sornom  10237  fin23lem16  10295  fin23lem20  10297  isf32lem2  10314  axcc2lem  10396  axdc3lem2  10411  ttukeylem6  10474  konigthlem  10528  pwcfsdom  10543  pwfseqlem1  10618  gch2  10635  1nn  12204  peano2nn  12205  rpnnen1lem5  12947  om2uzrani  13924  uzrdglem  13929  uzrdg0i  13931  fseqsupubi  13950  ccatrn  14561  uzin2  15318  climsup  15643  ruclem12  16216  0ram  16998  setcepi  18057  acsmapd  18520  cycsubgcl  19145  ghmrn  19168  conjnmz  19191  pmtrrn  19394  sylow1lem4  19538  pgpssslw  19551  sylow2blem3  19559  sylow3lem2  19565  efgsfo  19676  gexex  19790  gsumval3eu  19841  gsumzsplit  19864  pjfo  21631  issubassa2  21808  mplbas2  21956  mpfconst  22015  mpfproj  22016  mpfind  22021  pf1const  22240  pf1id  22241  mpfpf1  22245  pf1mpf  22246  toprntopon  22819  cmpsub  23294  conncn  23320  2ndcctbss  23349  2ndcdisj  23350  2ndcsep  23353  iskgen2  23442  kgen2cn  23453  ptbasfi  23475  ptcnplem  23515  isr0  23631  r0cld  23632  zfbas  23790  uzrest  23791  rnelfm  23847  tmdgsum2  23990  evth  24865  bcth3  25238  ivthicc  25366  ovolmge0  25385  ovollb2lem  25396  ovolunlem1a  25404  ovoliunlem1  25410  ovoliun  25413  ovolicc2lem4  25428  voliunlem1  25458  voliunlem3  25460  volsup  25464  ioombl1lem2  25467  ioombl1lem4  25469  uniioombllem2  25491  uniioombllem3  25493  vitalilem2  25517  vitalilem4  25519  mbflimsup  25574  itg11  25599  i1faddlem  25601  i1fmullem  25602  itg1mulc  25612  i1fres  25613  itg1climres  25622  mbfi1fseqlem3  25625  itg2seq  25650  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2cnlem1  25669  limciun  25802  dvcnvlem  25887  dvivthlem2  25921  dvivth  25922  lhop1lem  25925  lhop1  25926  lhop2  25927  aalioulem3  26249  basellem3  27000  nodenselem8  27610  noseq0  28191  noseqp1  28192  noseqrdg0  28208  tgelrnln  28564  wlkiswwlks1  29804  ubthlem1  30806  pjrni  31638  pjoi0  31653  hmopidmchi  32087  hmopidmpji  32088  pjssdif1i  32111  dfpjop  32118  pjadj3  32124  elpjrn  32126  pjcmul1i  32137  pjcmul2i  32138  pj3si  32143  ofrn2  32571  prodindf  32793  mgcf1o  32936  cycpmfvlem  33076  cycpmfv1  33077  cycpmfv2  33078  locfinreflem  33837  cnre2csqlem  33907  elmrsubrn  35514  elmsubrn  35522  msubrn  35523  elmsta  35542  vhmcls  35560  mclsppslem  35577  neibastop2lem  36355  tailfb  36372  fvineqsneu  37406  ptrecube  37621  heicant  37656  mblfinlem2  37659  ftc1anclem7  37700  ftc1anc  37702  sstotbnd2  37775  prdsbnd  37794  heibor1lem  37810  heiborlem1  37812  dihcl  41271  dih0rn  41285  dih1dimatlem  41330  dihlspsnssN  41333  dochocss  41367  hdmaprnlem17N  41864  hgmaprnlem1N  41897  nacsfix  42707  kercvrlsm  43079  pwssplit4  43085  tfsconcatrev  43344  orbitinit  44953  orbitcl  44954  climinf  45611  climinf2lem  45711  limsupvaluz2  45743  supcnvlimsup  45745  fourierdlem25  46137  fourierdlem42  46154  fourierdlem54  46165  fourierdlem64  46175  fourierdlem65  46176  sge0le  46412  sge0seq  46451  imaelsetpreimafv  47400