Theorem ffvelcdm 5768

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ran crn 4720   Fn wfn 5313  ⟶wf 5314  ‘cfv 5318

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-fv 5326

This theorem is referenced by:  ffvelcdmi  5769  ffvelcdmda  5770  dffo3  5782  ffnfv  5793  ffvresb  5798  fcompt  5805  fsn2  5809  fvconst  5827  foco2  5877  fcofo  5908  cocan1  5911  isocnv  5935  isores2  5937  isopolem  5946  isosolem  5948  fovcdm  6148  off  6231  mapsncnv  6842  2dom  6958  dom1o  6977  enm  6979  xpdom2  6990  xpmapenlem  7010  fiintim  7093  isotilem  7173  updjudhf  7246  exmidomniim  7308  finacn  7386  seqf1og  10743  shftf  11341  summodclem2a  11892  isumcl  11936  mertenslem2  12047  3dvds  12375  nn0seqcvgd  12563  algrf  12567  eucalg  12581  phimullem  12747  pcmpt  12866  pcprod  12869  imasaddfnlemg  13347  imasaddflemg  13349  mhmpropd  13499  ghmsub  13788  znunit  14623  upxp  14946  uptx  14948  txhmeo  14993  cncfmet  15266  dvaddxxbr  15375  dvcj  15383  dvfre  15384  plyf  15411  plyaddlem  15423  plymullem  15424  plycolemc  15432  plyreres  15438  dvply1  15439  lgsdir  15714  lgsdi  15716  lgseisenlem3  15751  bj-charfunr  16173