Theorem ffvelcdmda 5814

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ⟶wf 5350  ‘cfv 5354

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 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3045  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-fv 5362

This theorem is referenced by:  ffvelcdmd  5815  f1ocnvdm  5956  foeqcnvco  5965  f1oiso2  6002  offeq  6282  suppssof1  6286  ofco  6287  caofref  6293  caofinvl  6294  caofid0l  6295  caofid0r  6296  caofid1  6297  caofid2  6298  caofcom  6299  caofrss  6300  caoftrn  6301  caofdig  6302  suppssrst  6463  suppssrgst  6464  suppofss1dcl  6466  suppofss2dcl  6467  smofvon2dm  6529  smofvon  6532  pw2f1odclem  7089  mapxpen  7103  xpmapenlem  7104  en2eqpr  7169  supisoex  7302  ordiso2  7328  omp1eomlem  7387  ctssdccl  7404  ctssdc  7406  enumctlemm  7407  enomnilem  7431  fodjuomnilemdc  7437  ismkvnex  7448  enmkvlem  7454  enwomnilem  7462  nninfwlporlemd  7465  nninfwlporlem  7466  nninfwlpoimlemginf  7469  cc3  7584  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  caucvgprlemladdrl  7995  caucvgprprlemopu  8016  caucvgprprlemexbt  8023  caucvgprprlemexb  8024  caucvgsrlemcl  8106  caucvgsrlemfv  8108  caucvgsrlemcau  8110  caucvgsrlembound  8111  caucvgsrlemoffval  8113  caucvgsrlemofff  8114  caucvgsrlemoffgt1  8116  caucvgsrlemoffres  8117  caucvgsr  8119  axcaucvglemcl  8212  ofnegsub  9238  frecuzrdgfunlem  10785  monoord2  10852  seq3f1o  10883  seqf1oglem2  10886  seqf1og  10887  seq3homo  10893  seqfeq3  10895  zfz1isolemiso  11215  seq3coll  11218  wrdsymbcl  11242  ccatcl  11285  resqrexlemfp1  11698  resqrexlemover  11699  resqrexlemdec  11700  resqrexlemlo  11702  resqrexlemcalc1  11703  resqrexlemcalc2  11704  resqrexlemcalc3  11705  resqrexlemgt0  11709  resqrexlemsqa  11713  clim2ser  12026  clim2ser2  12027  isermulc2  12029  iserle  12031  climserle  12034  climrecvg1n  12037  climcvg1nlem  12038  summodclem3  12070  summodclem2a  12071  fsumgcl  12076  fsum3  12077  fsumf1o  12080  isumss  12081  fisumss  12082  fsumcl2lem  12088  fsumadd  12096  isumclim3  12113  isummulc2  12116  isumrecl  12119  isumadd  12121  fsummulc2  12138  iserabs  12165  cvgcmpub  12166  isumshft  12180  isumsplit  12181  mertensabs  12227  clim2prod  12229  clim2divap  12230  prodfap0  12235  prodfdivap  12237  prodmodclem3  12265  prodmodclem2a  12266  fprodseq  12273  fprodf1o  12278  prodssdc  12279  fprodssdc  12280  fprodmul  12281  efcj  12363  nninfctlemfo  12740  nn0seqcvgd  12742  algrp1  12747  alginv  12748  algcvg  12749  algcvga  12752  algfx  12753  eucalgcvga  12759  eulerthlem1  12928  eulerthlemh  12932  eulerthlemth  12933  pcmptcl  13044  pcmpt  13045  1arithlem4  13068  nninfdclemf1  13220  prdsplusgsgrpcl  13644  prdssgrpd  13645  prdsplusgcl  13676  prdsidlem  13677  prdsmndd  13678  gsumwsubmcl  13726  gsumwmhm  13728  grpinvcl  13778  prdsinvlem  13838  pwsinvg  13842  pwssub  13843  mhmmulg  13897  ghminv  13984  gsumfzreidx  14071  gsumfzsubmcl  14072  gsumfzmptfidmadd  14073  gsumfzmhm  14077  rhmdvdsr  14337  rrgsupp  14428  psrbagcon  14843  psrbagconf1o  14845  psrlinv  14856  psr1clfi  14860  mplsubgfilemcl  14871  cnptoprest2  15122  lmss  15128  txcnmpt  15155  txlm  15161  lmcn2  15162  psmetxrge0  15214  metcnp  15394  climcncf  15466  negfcncf  15488  ivthdec  15526  ivthreinc  15527  dvcnp2cntop  15581  dvaddxxbr  15583  dvimulf  15588  dvcj  15591  dvfre  15592  elply2  15617  plyaddlem1  15629  plymullem1  15630  plycolemc  15640  plyco  15641  dvply2g  15648  lgscllem  15897  lgsfle1  15899  lgsval4a  15912  lgsneg  15914  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  uhgrss  16087  uhgrm  16090  upgrss  16111  upgrm  16112  upgr1or2  16113  umgredg2en  16121  lfgredg2dom  16144  usgrss  16189  depindlem1  16518  depindlem2  16519  pw1map  16786  nninfall  16804  nninffeq  16815  refeq  16825  trilpolemclim  16837  trilpolemcl  16838  trilpolemisumle  16839  trilpolemeq1  16841  iswomni0  16853