Theorem fnfvelrn 7034

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5632   Fn wfn 6494  ‘cfv 6499

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6452  df-fun 6501  df-fn 6502  df-fv 6507

This theorem is referenced by:  ffvelcdm  7035  fnfvelrnd  7036  fvcofneq  7047  fnovrn  7544  offvalfv  7655  fo1stres  7973  fo2ndres  7974  offsplitfpar  8075  fo2ndf  8077  seqomlem3  8397  seqomlem4  8398  phplem2  9146  indexfi  9287  dffi3  9358  ordtypelem7  9453  inf0  9550  infdifsn  9586  noinfep  9589  cantnflem3  9620  cantnf  9622  cardinfima  10026  alephfplem1  10033  alephfplem3  10035  alephfp  10037  dfac5  10058  dfac12lem2  10074  cfflb  10188  sornom  10206  fin23lem16  10264  fin23lem20  10266  isf32lem2  10283  axcc2lem  10365  axdc3lem2  10380  ttukeylem6  10443  konigthlem  10497  pwcfsdom  10512  pwfseqlem1  10587  gch2  10604  1nn  12173  peano2nn  12174  rpnnen1lem5  12916  om2uzrani  13893  uzrdglem  13898  uzrdg0i  13900  fseqsupubi  13919  ccatrn  14530  uzin2  15287  climsup  15612  ruclem12  16185  0ram  16967  setcepi  18026  acsmapd  18489  cycsubgcl  19114  ghmrn  19137  conjnmz  19160  pmtrrn  19363  sylow1lem4  19507  pgpssslw  19520  sylow2blem3  19528  sylow3lem2  19534  efgsfo  19645  gexex  19759  gsumval3eu  19810  gsumzsplit  19833  pjfo  21600  issubassa2  21777  mplbas2  21925  mpfconst  21984  mpfproj  21985  mpfind  21990  pf1const  22209  pf1id  22210  mpfpf1  22214  pf1mpf  22215  toprntopon  22788  cmpsub  23263  conncn  23289  2ndcctbss  23318  2ndcdisj  23319  2ndcsep  23322  iskgen2  23411  kgen2cn  23422  ptbasfi  23444  ptcnplem  23484  isr0  23600  r0cld  23601  zfbas  23759  uzrest  23760  rnelfm  23816  tmdgsum2  23959  evth  24834  bcth3  25207  ivthicc  25335  ovolmge0  25354  ovollb2lem  25365  ovolunlem1a  25373  ovoliunlem1  25379  ovoliun  25382  ovolicc2lem4  25397  voliunlem1  25427  voliunlem3  25429  volsup  25433  ioombl1lem2  25436  ioombl1lem4  25438  uniioombllem2  25460  uniioombllem3  25462  vitalilem2  25486  vitalilem4  25488  mbflimsup  25543  itg11  25568  i1faddlem  25570  i1fmullem  25571  itg1mulc  25581  i1fres  25582  itg1climres  25591  mbfi1fseqlem3  25594  itg2seq  25619  itg2monolem2  25628  itg2monolem3  25629  itg2mono  25630  itg2cnlem1  25638  limciun  25771  dvcnvlem  25856  dvivthlem2  25890  dvivth  25891  lhop1lem  25894  lhop1  25895  lhop2  25896  aalioulem3  26218  basellem3  26969  nodenselem8  27579  noseq0  28160  noseqp1  28161  noseqrdg0  28177  tgelrnln  28533  wlkiswwlks1  29770  ubthlem1  30772  pjrni  31604  pjoi0  31619  hmopidmchi  32053  hmopidmpji  32054  pjssdif1i  32077  dfpjop  32084  pjadj3  32090  elpjrn  32092  pjcmul1i  32103  pjcmul2i  32104  pj3si  32109  ofrn2  32537  prodindf  32759  mgcf1o  32902  cycpmfvlem  33042  cycpmfv1  33043  cycpmfv2  33044  locfinreflem  33803  cnre2csqlem  33873  elmrsubrn  35480  elmsubrn  35488  msubrn  35489  elmsta  35508  vhmcls  35526  mclsppslem  35543  neibastop2lem  36321  tailfb  36338  fvineqsneu  37372  ptrecube  37587  heicant  37622  mblfinlem2  37625  ftc1anclem7  37666  ftc1anc  37668  sstotbnd2  37741  prdsbnd  37760  heibor1lem  37776  heiborlem1  37778  dihcl  41237  dih0rn  41251  dih1dimatlem  41296  dihlspsnssN  41299  dochocss  41333  hdmaprnlem17N  41830  hgmaprnlem1N  41863  nacsfix  42673  kercvrlsm  43045  pwssplit4  43051  tfsconcatrev  43310  orbitinit  44919  orbitcl  44920  climinf  45577  climinf2lem  45677  limsupvaluz2  45709  supcnvlimsup  45711  fourierdlem25  46103  fourierdlem42  46120  fourierdlem54  46131  fourierdlem64  46141  fourierdlem65  46142  sge0le  46378  sge0seq  46417  imaelsetpreimafv  47369