Theorem ffvelrni 6850

Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)

Hypothesis

Ref	Expression
ffvrni.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

Ref	Expression
ffvelrni	⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelrni

Step	Hyp	Ref	Expression
1		ffvrni.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		ffvelrn 6849	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 688	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114  ⟶wf 6351  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363

This theorem is referenced by:  f0cli  6864  cantnfval2  9132  cantnfle  9134  cantnflt  9135  cantnfres  9140  cantnfp1lem3  9143  cantnflem1b  9149  cantnflem1d  9151  cantnflem1  9152  wemapwe  9160  cnfcomlem  9162  cnfcom  9163  cnfcom3lem  9166  cnfcom3  9167  ackbij1lem14  9655  ackbij1lem15  9656  ackbij1lem16  9657  ackbij1lem18  9659  fpwwe2lem8  10059  nqercl  10353  uzssz  12265  axdc4uzlem  13352  hashkf  13693  hashcl  13718  hashxrcl  13719  hashgadd  13739  cjcl  14464  limsupcl  14830  limsuplt  14836  limsupval2  14837  limsupgre  14838  limsupbnd2  14840  cn1lem  14954  climcn1lem  14959  caucvgrlem2  15031  fsumrelem  15162  ackbijnn  15183  efcl  15436  sincl  15479  coscl  15480  rpnnen2lem9  15575  rpnnen2lem12  15578  sadcaddlem  15806  sadadd2lem  15808  sadadd3  15810  sadaddlem  15815  sadasslem  15819  sadeq  15821  algcvg  15920  algcvgb  15922  algcvga  15923  algfx  15924  eucalgcvga  15930  eucalg  15931  xpsaddlem  16846  xpsvsca  16850  xpsle  16852  efgtf  18848  efgtlen  18852  efginvrel2  18853  efginvrel1  18854  efgsp1  18863  efgredleme  18869  efgredlemc  18871  efgred  18874  efgred2  18879  efgcpbllemb  18881  frgpnabllem1  18993  xpsdsval  22991  xrhmeo  23550  ioorcl  24178  volsup2  24206  volivth  24208  itg2const2  24342  itg2gt0  24361  dvcjbr  24546  dvcj  24547  dvfre  24548  rolle  24587  deg1xrcl  24676  plypf1  24802  resinf1o  25120  efif1olem4  25129  eff1olem  25132  logrncl  25151  relogcl  25159  asincl  25451  acoscl  25453  atancl  25459  asinrebnd  25479  dvatan  25513  leibpilem2  25519  leibpi  25520  areacl  25540  areage0  25541  divsqrtsumo1  25561  emcllem6  25578  emcllem7  25579  gamcl  25621  chtcl  25686  chpcl  25701  ppicl  25708  mucl  25718  sqff1o  25759  bposlem7  25866  dchrisum0lem2a  26093  mulog2sumlem1  26110  pntrsumo1  26141  pntrsumbnd  26142  pntrsumbnd2  26143  selbergr  26144  selberg3r  26145  selberg34r  26147  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2  26167  pntlemn  26176  pntlemj  26179  pntlemf  26181  pntlemo  26183  pntleml  26187  lnocoi  28534  nmlno0lem  28570  nmblolbii  28576  blocnilem  28581  blocni  28582  normcl  28902  occl  29081  hococli  29542  hosubcli  29546  hoaddcomi  29549  hodsi  29552  hoaddassi  29553  hocadddiri  29556  hocsubdiri  29557  ho2coi  29558  hoaddid1i  29563  ho0coi  29565  hoid1ri  29567  honegsubi  29573  ho01i  29605  ho02i  29606  dmadjrn  29672  nmopnegi  29742  lnopaddi  29748  lnopsubi  29751  hoddii  29766  nmlnop0iALT  29772  lnopmi  29777  lnophsi  29778  lnopcoi  29780  lnopeq0lem1  29782  lnopeqi  29785  lnopunilem1  29787  lnopunilem2  29788  lnophmlem2  29794  nmbdoplbi  29801  nmcopexi  29804  nmcoplbi  29805  nmophmi  29808  lnopconi  29811  lnfn0i  29819  lnfnaddi  29820  lnfnmuli  29821  lnfnsubi  29823  nmbdfnlbi  29826  nmcfnexi  29828  nmcfnlbi  29829  lnfnconi  29832  riesz3i  29839  riesz4i  29840  cnlnadjlem2  29845  cnlnadjlem4  29847  cnlnadjlem6  29849  cnlnadjlem7  29850  nmopadjlem  29866  nmoptrii  29871  nmopcoi  29872  adjcoi  29877  nmopcoadji  29878  bracnln  29886  opsqrlem5  29921  opsqrlem6  29922  hmopidmchi  29928  hmopidmpji  29929  pjsdii  29932  pjddii  29933  pjcohocli  29980  mhmhmeotmd  31170  xrge0pluscn  31183  voliune  31488  volfiniune  31489  ddemeas  31495  eulerpartlems  31618  eulerpartlemsv3  31619  eulerpartlemgc  31620  eulerpartlemgvv  31634  eulerpartlemgf  31637  eulerpartlemgs2  31638  eulerpartlemn  31639  derangen  32419  subfacf  32422  subfacp1lem6  32432  subfaclim  32435  subfacval3  32436  msrrcl  32790  msrid  32792  circum  32917  liminfval2  42098  ismbl3  42320  ovolsplit  42322  stirlinglem13  42420  fourierdlem55  42495  fourierdlem77  42517  fourierdlem80  42520