Theorem ffvelcdm 5634

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 5350	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 5633	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 282	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 5359	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3148	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 275	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 13	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2143  ran crn 4614   Fn wfn 5196  ⟶wf 5197  ‘cfv 5201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 706  ax-5 1442  ax-7 1443  ax-gen 1444  ax-ie1 1488  ax-ie2 1489  ax-8 1499  ax-10 1500  ax-11 1501  ax-i12 1502  ax-bndl 1504  ax-4 1505  ax-17 1521  ax-i9 1525  ax-ial 1529  ax-i5r 1530  ax-14 2146  ax-ext 2154  ax-sep 4109  ax-pow 4162  ax-pr 4196

This theorem depends on definitions:  df-bi 116  df-3an 977  df-tru 1353  df-nf 1456  df-sb 1758  df-eu 2024  df-mo 2025  df-clab 2159  df-cleq 2165  df-clel 2168  df-nfc 2303  df-ral 2455  df-rex 2456  df-v 2734  df-sbc 2958  df-un 3127  df-in 3129  df-ss 3136  df-pw 3570  df-sn 3591  df-pr 3592  df-op 3594  df-uni 3799  df-br 3992  df-opab 4053  df-id 4280  df-xp 4619  df-rel 4620  df-cnv 4621  df-co 4622  df-dm 4623  df-rn 4624  df-iota 5163  df-fun 5203  df-fn 5204  df-f 5205  df-fv 5209

This theorem is referenced by:  ffvelrni  5635  ffvelrnda  5636  dffo3  5648  ffnfv  5659  ffvresb  5664  fcompt  5671  fsn2  5675  fvconst  5689  foco2  5738  fcofo  5768  cocan1  5771  isocnv  5795  isores2  5797  isopolem  5806  isosolem  5808  fovrn  6000  off  6078  mapsncnv  6678  2dom  6788  enm  6803  xpdom2  6814  xpmapenlem  6832  fiintim  6911  isotilem  6988  updjudhf  7061  exmidomniim  7122  shftf  10799  summodclem2a  11349  isumcl  11393  mertenslem2  11504  nn0seqcvgd  12000  algrf  12004  eucalg  12018  phimullem  12184  pcmpt  12300  pcprod  12303  mhmpropd  12694  upxp  13110  uptx  13112  txhmeo  13157  cncfmet  13417  dvaddxxbr  13503  dvcj  13511  dvfre  13512  lgsdir  13774  lgsdi  13776  bj-charfunr  13889