Theorem ffvelcdm 5713

Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)

Assertion

Ref	Expression
ffvelcdm	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdm

Step	Hyp	Ref	Expression
1		ffn 5425	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 5712	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 283	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 5434	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3192	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 276	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 13	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2176  ran crn 4676   Fn wfn 5266  ⟶wf 5267  ‘cfv 5271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-opab 4106  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279

This theorem is referenced by:  ffvelcdmi  5714  ffvelcdmda  5715  dffo3  5727  ffnfv  5738  ffvresb  5743  fcompt  5750  fsn2  5754  fvconst  5772  foco2  5822  fcofo  5853  cocan1  5856  isocnv  5880  isores2  5882  isopolem  5891  isosolem  5893  fovcdm  6089  off  6171  mapsncnv  6782  2dom  6897  enm  6915  xpdom2  6926  xpmapenlem  6946  fiintim  7028  isotilem  7108  updjudhf  7181  exmidomniim  7243  finacn  7316  seqf1og  10666  shftf  11141  summodclem2a  11692  isumcl  11736  mertenslem2  11847  3dvds  12175  nn0seqcvgd  12363  algrf  12367  eucalg  12381  phimullem  12547  pcmpt  12666  pcprod  12669  imasaddfnlemg  13146  imasaddflemg  13148  mhmpropd  13298  ghmsub  13587  znunit  14421  upxp  14744  uptx  14746  txhmeo  14791  cncfmet  15064  dvaddxxbr  15173  dvcj  15181  dvfre  15182  plyf  15209  plyaddlem  15221  plymullem  15222  plycolemc  15230  plyreres  15236  dvply1  15237  lgsdir  15512  lgsdi  15514  lgseisenlem3  15549  bj-charfunr  15746