Theorem fnfvelrn 6356

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990  ran crn 5115   Fn wfn 5883  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896

This theorem is referenced by:  ffvelrn  6357  fvcofneq  6367  fnovrn  6809  fo1stres  7192  fo2ndres  7193  fo2ndf  7284  seqomlem3  7547  seqomlem4  7548  phplem4  8142  indexfi  8274  dffi3  8337  ordtypelem7  8429  inf0  8518  infdifsn  8554  noinfep  8557  cantnflem3  8588  cantnf  8590  cardinfima  8920  alephfplem1  8927  alephfplem3  8929  alephfp  8931  dfac5  8951  dfac12lem2  8966  cfflb  9081  sornom  9099  fin23lem16  9157  fin23lem20  9159  isf32lem2  9176  axcc2lem  9258  axdc3lem2  9273  ttukeylem6  9336  konigthlem  9390  pwcfsdom  9405  pwfseqlem1  9480  gch2  9497  1nn  11031  peano2nn  11032  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  om2uzrani  12751  uzrdglem  12756  uzrdg0i  12758  fseqsupubi  12777  ccatrn  13372  uzin2  14084  climsup  14400  ruclem12  14970  0ram  15724  setcepi  16738  acsmapd  17178  cycsubgcl  17620  ghmrn  17673  conjnmz  17694  pmtrrn  17877  sylow1lem4  18016  pgpssslw  18029  sylow2blem3  18037  sylow3lem2  18043  efgsfo  18152  gexex  18256  gsumval3eu  18305  gsumzsplit  18327  issubassa2  19345  mplbas2  19470  mpfconst  19530  mpfproj  19531  mpfind  19536  pf1const  19710  pf1id  19711  mpfpf1  19715  pf1mpf  19716  pjfo  20059  toprntopon  20729  cmpsub  21203  conncn  21229  2ndcctbss  21258  2ndcdisj  21259  2ndcsep  21262  iskgen2  21351  kgen2cn  21362  ptbasfi  21384  ptcnplem  21424  isr0  21540  r0cld  21541  zfbas  21700  uzrest  21701  rnelfm  21757  tmdgsum2  21900  evth  22758  bcth3  23128  ivthicc  23227  ovolmge0  23245  ovollb2lem  23256  ovolunlem1a  23264  ovoliunlem1  23270  ovoliun  23273  ovolicc2lem4  23288  voliunlem1  23318  voliunlem3  23320  volsup  23324  ioombl1lem2  23327  ioombl1lem4  23329  uniioombllem2  23351  uniioombllem3  23353  vitalilem2  23378  vitalilem4  23380  mbflimsup  23433  itg11  23458  i1faddlem  23460  i1fmullem  23461  itg1mulc  23471  i1fres  23472  itg1climres  23481  mbfi1fseqlem3  23484  itg2seq  23509  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  itg2cnlem1  23528  limciun  23658  dvcnvlem  23739  dvivthlem2  23772  dvivth  23773  lhop1lem  23776  lhop1  23777  lhop2  23778  aalioulem3  24089  basellem3  24809  tgelrnln  25525  wlkiswwlks1  26753  ubthlem1  27726  pjrni  28561  pjoi0  28576  hmopidmchi  29010  hmopidmpji  29011  pjssdif1i  29034  dfpjop  29041  pjadj3  29047  elpjrn  29049  pjcmul1i  29060  pjcmul2i  29061  pj3si  29066  ofrn2  29442  locfinreflem  29907  cnre2csqlem  29956  prodindf  30085  elmrsubrn  31417  elmsubrn  31425  msubrn  31426  elmsta  31445  vhmcls  31463  mclsppslem  31480  nodenselem8  31841  neibastop2lem  32355  tailfb  32372  ptrecube  33409  heicant  33444  mblfinlem2  33447  ftc1anclem7  33491  ftc1anc  33493  sstotbnd2  33573  prdsbnd  33592  heibor1lem  33608  heiborlem1  33610  dihcl  36559  dih0rn  36573  dih1dimatlem  36618  dihlspsnssN  36621  dochocss  36655  hdmaprnlem17N  37155  hgmaprnlem1N  37188  nacsfix  37275  kercvrlsm  37653  pwssplit4  37659  ssmapsn  39408  fnfvelrnd  39479  climinf  39838  climinf2lem  39938  limsupvaluz2  39970  supcnvlimsup  39972  fourierdlem25  40349  fourierdlem42  40366  fourierdlem54  40377  fourierdlem64  40387  fourierdlem65  40388  sge0le  40624  sge0seq  40663  offvalfv  42121