Theorem ffvelcdmda 5714

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 5712	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	sylan 283	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2175  ⟶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:  ffvelcdmd  5715  f1ocnvdm  5849  foeqcnvco  5858  f1oiso2  5895  offeq  6171  suppssof1  6175  ofco  6176  caofref  6182  caofinvl  6183  caofid0l  6184  caofid0r  6185  caofid1  6186  caofid2  6187  caofcom  6188  caofrss  6189  caoftrn  6190  caofdig  6191  smofvon2dm  6381  smofvon  6384  pw2f1odclem  6930  mapxpen  6944  xpmapenlem  6945  en2eqpr  7003  supisoex  7110  ordiso2  7136  omp1eomlem  7195  ctssdccl  7212  ctssdc  7214  enumctlemm  7215  enomnilem  7239  fodjuomnilemdc  7245  ismkvnex  7256  enmkvlem  7262  enwomnilem  7270  nninfwlporlemd  7273  nninfwlporlem  7274  nninfwlpoimlemginf  7277  cc3  7379  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  caucvgprlemladdrl  7790  caucvgprprlemopu  7811  caucvgprprlemexbt  7818  caucvgprprlemexb  7819  caucvgsrlemcl  7901  caucvgsrlemfv  7903  caucvgsrlemcau  7905  caucvgsrlembound  7906  caucvgsrlemoffval  7908  caucvgsrlemofff  7909  caucvgsrlemoffgt1  7911  caucvgsrlemoffres  7912  caucvgsr  7914  axcaucvglemcl  8007  ofnegsub  9034  frecuzrdgfunlem  10562  monoord2  10629  seq3f1o  10660  seqf1oglem2  10663  seqf1og  10664  seq3homo  10670  seqfeq3  10672  zfz1isolemiso  10982  seq3coll  10985  wrdsymbcl  11006  ccatcl  11047  resqrexlemfp1  11291  resqrexlemover  11292  resqrexlemdec  11293  resqrexlemlo  11295  resqrexlemcalc1  11296  resqrexlemcalc2  11297  resqrexlemcalc3  11298  resqrexlemgt0  11302  resqrexlemsqa  11306  clim2ser  11619  clim2ser2  11620  isermulc2  11622  iserle  11624  climserle  11627  climrecvg1n  11630  climcvg1nlem  11631  summodclem3  11662  summodclem2a  11663  fsumgcl  11668  fsum3  11669  fsumf1o  11672  isumss  11673  fisumss  11674  fsumcl2lem  11680  fsumadd  11688  isumclim3  11705  isummulc2  11708  isumrecl  11711  isumadd  11713  fsummulc2  11730  iserabs  11757  cvgcmpub  11758  isumshft  11772  isumsplit  11773  mertensabs  11819  clim2prod  11821  clim2divap  11822  prodfap0  11827  prodfdivap  11829  prodmodclem3  11857  prodmodclem2a  11858  fprodseq  11865  fprodf1o  11870  prodssdc  11871  fprodssdc  11872  fprodmul  11873  efcj  11955  nninfctlemfo  12332  nn0seqcvgd  12334  algrp1  12339  alginv  12340  algcvg  12341  algcvga  12344  algfx  12345  eucalgcvga  12351  eulerthlem1  12520  eulerthlemh  12524  eulerthlemth  12525  pcmptcl  12636  pcmpt  12637  1arithlem4  12660  nninfdclemf1  12794  prdsplusgsgrpcl  13217  prdssgrpd  13218  prdsplusgcl  13249  prdsidlem  13250  prdsmndd  13251  gsumwsubmcl  13299  gsumwmhm  13301  grpinvcl  13351  prdsinvlem  13411  pwsinvg  13415  pwssub  13416  mhmmulg  13470  ghminv  13557  gsumfzreidx  13644  gsumfzsubmcl  13645  gsumfzmptfidmadd  13646  gsumfzmhm  13650  rhmdvdsr  13908  psrlinv  14417  psr1clfi  14421  mplsubgfilemcl  14432  cnptoprest2  14683  lmss  14689  txcnmpt  14716  txlm  14722  lmcn2  14723  psmetxrge0  14775  metcnp  14955  climcncf  15027  negfcncf  15049  ivthdec  15087  ivthreinc  15088  dvcnp2cntop  15142  dvaddxxbr  15144  dvimulf  15149  dvcj  15152  dvfre  15153  elply2  15178  plyaddlem1  15190  plymullem1  15191  plycolemc  15201  plyco  15202  dvply2g  15209  lgscllem  15455  lgsfle1  15457  lgsval4a  15470  lgsneg  15472  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486  nninfall  15908  nninffeq  15919  refeq  15929  trilpolemclim  15937  trilpolemcl  15938  trilpolemisumle  15939  trilpolemeq1  15941  iswomni0  15952