Theorem ffvelcdmda 5812

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypothesis

Ref	Expression
ffvelcdmd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
ffvelcdmda	⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdmda

Step	Hyp	Ref	Expression
1		ffvelcdmd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffvelcdm 5810	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	sylan 283	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  ⟶wf 5348  ‘cfv 5352

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-sbc 3043  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-rn 4760  df-iota 5312  df-fun 5354  df-fn 5355  df-f 5356  df-fv 5360

This theorem is referenced by:  ffvelcdmd  5813  f1ocnvdm  5954  foeqcnvco  5963  f1oiso2  6000  offeq  6280  suppssof1  6284  ofco  6285  caofref  6291  caofinvl  6292  caofid0l  6293  caofid0r  6294  caofid1  6295  caofid2  6296  caofcom  6297  caofrss  6298  caoftrn  6299  caofdig  6300  suppssrst  6461  suppssrgst  6462  suppofss1dcl  6464  suppofss2dcl  6465  smofvon2dm  6527  smofvon  6530  pw2f1odclem  7087  mapxpen  7101  xpmapenlem  7102  en2eqpr  7167  supisoex  7300  ordiso2  7326  omp1eomlem  7385  ctssdccl  7402  ctssdc  7404  enumctlemm  7405  enomnilem  7429  fodjuomnilemdc  7435  ismkvnex  7446  enmkvlem  7452  enwomnilem  7460  nninfwlporlemd  7463  nninfwlporlem  7464  nninfwlpoimlemginf  7467  cc3  7582  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemladdrl  7993  caucvgprprlemopu  8014  caucvgprprlemexbt  8021  caucvgprprlemexb  8022  caucvgsrlemcl  8104  caucvgsrlemfv  8106  caucvgsrlemcau  8108  caucvgsrlembound  8109  caucvgsrlemoffval  8111  caucvgsrlemofff  8112  caucvgsrlemoffgt1  8114  caucvgsrlemoffres  8115  caucvgsr  8117  axcaucvglemcl  8210  ofnegsub  9236  frecuzrdgfunlem  10781  monoord2  10848  seq3f1o  10879  seqf1oglem2  10882  seqf1og  10883  seq3homo  10889  seqfeq3  10891  zfz1isolemiso  11211  seq3coll  11214  wrdsymbcl  11238  ccatcl  11281  resqrexlemfp1  11694  resqrexlemover  11695  resqrexlemdec  11696  resqrexlemlo  11698  resqrexlemcalc1  11699  resqrexlemcalc2  11700  resqrexlemcalc3  11701  resqrexlemgt0  11705  resqrexlemsqa  11709  clim2ser  12022  clim2ser2  12023  isermulc2  12025  iserle  12027  climserle  12030  climrecvg1n  12033  climcvg1nlem  12034  summodclem3  12066  summodclem2a  12067  fsumgcl  12072  fsum3  12073  fsumf1o  12076  isumss  12077  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  isumclim3  12109  isummulc2  12112  isumrecl  12115  isumadd  12117  fsummulc2  12134  iserabs  12161  cvgcmpub  12162  isumshft  12176  isumsplit  12177  mertensabs  12223  clim2prod  12225  clim2divap  12226  prodfap0  12231  prodfdivap  12233  prodmodclem3  12261  prodmodclem2a  12262  fprodseq  12269  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodmul  12277  efcj  12359  nninfctlemfo  12736  nn0seqcvgd  12738  algrp1  12743  alginv  12744  algcvg  12745  algcvga  12748  algfx  12749  eucalgcvga  12755  eulerthlem1  12924  eulerthlemh  12928  eulerthlemth  12929  pcmptcl  13040  pcmpt  13041  1arithlem4  13064  nninfdclemf1  13203  prdsplusgsgrpcl  13627  prdssgrpd  13628  prdsplusgcl  13659  prdsidlem  13660  prdsmndd  13661  gsumwsubmcl  13709  gsumwmhm  13711  grpinvcl  13761  prdsinvlem  13821  pwsinvg  13825  pwssub  13826  mhmmulg  13880  ghminv  13967  gsumfzreidx  14054  gsumfzsubmcl  14055  gsumfzmptfidmadd  14056  gsumfzmhm  14060  rhmdvdsr  14320  rrgsupp  14411  psrbagcon  14826  psrbagconf1o  14828  psrlinv  14839  psr1clfi  14843  mplsubgfilemcl  14854  cnptoprest2  15105  lmss  15111  txcnmpt  15138  txlm  15144  lmcn2  15145  psmetxrge0  15197  metcnp  15377  climcncf  15449  negfcncf  15471  ivthdec  15509  ivthreinc  15510  dvcnp2cntop  15564  dvaddxxbr  15566  dvimulf  15571  dvcj  15574  dvfre  15575  elply2  15600  plyaddlem1  15612  plymullem1  15613  plycolemc  15623  plyco  15624  dvply2g  15631  lgscllem  15880  lgsfle1  15882  lgsval4a  15895  lgsneg  15897  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  uhgrss  16070  uhgrm  16073  upgrss  16094  upgrm  16095  upgr1or2  16096  umgredg2en  16104  lfgredg2dom  16127  usgrss  16172  depindlem1  16501  depindlem2  16502  pw1map  16769  nninfall  16787  nninffeq  16798  refeq  16808  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  iswomni0  16836