Theorem ffvelcdm 5736

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 5445	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 5735	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 283	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 5454	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3200	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 276	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 13	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2178  ran crn 4694   Fn wfn 5285  ⟶wf 5286  ‘cfv 5290

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-sbc 3006  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-opab 4122  df-id 4358  df-xp 4699  df-rel 4700  df-cnv 4701  df-co 4702  df-dm 4703  df-rn 4704  df-iota 5251  df-fun 5292  df-fn 5293  df-f 5294  df-fv 5298

This theorem is referenced by:  ffvelcdmi  5737  ffvelcdmda  5738  dffo3  5750  ffnfv  5761  ffvresb  5766  fcompt  5773  fsn2  5777  fvconst  5795  foco2  5845  fcofo  5876  cocan1  5879  isocnv  5903  isores2  5905  isopolem  5914  isosolem  5916  fovcdm  6112  off  6194  mapsncnv  6805  2dom  6921  enm  6940  xpdom2  6951  xpmapenlem  6971  fiintim  7054  isotilem  7134  updjudhf  7207  exmidomniim  7269  finacn  7347  seqf1og  10703  shftf  11256  summodclem2a  11807  isumcl  11851  mertenslem2  11962  3dvds  12290  nn0seqcvgd  12478  algrf  12482  eucalg  12496  phimullem  12662  pcmpt  12781  pcprod  12784  imasaddfnlemg  13261  imasaddflemg  13263  mhmpropd  13413  ghmsub  13702  znunit  14536  upxp  14859  uptx  14861  txhmeo  14906  cncfmet  15179  dvaddxxbr  15288  dvcj  15296  dvfre  15297  plyf  15324  plyaddlem  15336  plymullem  15337  plycolemc  15345  plyreres  15351  dvply1  15352  lgsdir  15627  lgsdi  15629  lgseisenlem3  15664  bj-charfunr  15945  dom1o  16128