Theorem ffvelcdm 5712

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2175  ran crn 4675   Fn wfn 5265  ⟶wf 5266  ‘cfv 5270

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-sbc 2998  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-rn 4685  df-iota 5231  df-fun 5272  df-fn 5273  df-f 5274  df-fv 5278

This theorem is referenced by:  ffvelcdmi  5713  ffvelcdmda  5714  dffo3  5726  ffnfv  5737  ffvresb  5742  fcompt  5749  fsn2  5753  fvconst  5771  foco2  5821  fcofo  5852  cocan1  5855  isocnv  5879  isores2  5881  isopolem  5890  isosolem  5892  fovcdm  6088  off  6170  mapsncnv  6781  2dom  6896  enm  6914  xpdom2  6925  xpmapenlem  6945  fiintim  7027  isotilem  7107  updjudhf  7180  exmidomniim  7242  finacn  7315  seqf1og  10664  shftf  11112  summodclem2a  11663  isumcl  11707  mertenslem2  11818  3dvds  12146  nn0seqcvgd  12334  algrf  12338  eucalg  12352  phimullem  12518  pcmpt  12637  pcprod  12640  imasaddfnlemg  13117  imasaddflemg  13119  mhmpropd  13269  ghmsub  13558  znunit  14392  upxp  14715  uptx  14717  txhmeo  14762  cncfmet  15035  dvaddxxbr  15144  dvcj  15152  dvfre  15153  plyf  15180  plyaddlem  15192  plymullem  15193  plycolemc  15201  plyreres  15207  dvply1  15208  lgsdir  15483  lgsdi  15485  lgseisenlem3  15520  bj-charfunr  15708