Theorem ffvelcdmda 5772

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ⟶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:  ffvelcdmd  5773  f1ocnvdm  5911  foeqcnvco  5920  f1oiso2  5957  offeq  6238  suppssof1  6242  ofco  6243  caofref  6249  caofinvl  6250  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  caofcom  6255  caofrss  6256  caoftrn  6257  caofdig  6258  smofvon2dm  6448  smofvon  6451  pw2f1odclem  7003  mapxpen  7017  xpmapenlem  7018  en2eqpr  7080  supisoex  7187  ordiso2  7213  omp1eomlem  7272  ctssdccl  7289  ctssdc  7291  enumctlemm  7292  enomnilem  7316  fodjuomnilemdc  7322  ismkvnex  7333  enmkvlem  7339  enwomnilem  7347  nninfwlporlemd  7350  nninfwlporlem  7351  nninfwlpoimlemginf  7354  cc3  7465  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  caucvgprprlemopu  7897  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsrlemcau  7991  caucvgsrlembound  7992  caucvgsrlemoffval  7994  caucvgsrlemofff  7995  caucvgsrlemoffgt1  7997  caucvgsrlemoffres  7998  caucvgsr  8000  axcaucvglemcl  8093  ofnegsub  9120  frecuzrdgfunlem  10653  monoord2  10720  seq3f1o  10751  seqf1oglem2  10754  seqf1og  10755  seq3homo  10761  seqfeq3  10763  zfz1isolemiso  11074  seq3coll  11077  wrdsymbcl  11098  ccatcl  11141  resqrexlemfp1  11535  resqrexlemover  11536  resqrexlemdec  11537  resqrexlemlo  11539  resqrexlemcalc1  11540  resqrexlemcalc2  11541  resqrexlemcalc3  11542  resqrexlemgt0  11546  resqrexlemsqa  11550  clim2ser  11863  clim2ser2  11864  isermulc2  11866  iserle  11868  climserle  11871  climrecvg1n  11874  climcvg1nlem  11875  summodclem3  11906  summodclem2a  11907  fsumgcl  11912  fsum3  11913  fsumf1o  11916  isumss  11917  fisumss  11918  fsumcl2lem  11924  fsumadd  11932  isumclim3  11949  isummulc2  11952  isumrecl  11955  isumadd  11957  fsummulc2  11974  iserabs  12001  cvgcmpub  12002  isumshft  12016  isumsplit  12017  mertensabs  12063  clim2prod  12065  clim2divap  12066  prodfap0  12071  prodfdivap  12073  prodmodclem3  12101  prodmodclem2a  12102  fprodseq  12109  fprodf1o  12114  prodssdc  12115  fprodssdc  12116  fprodmul  12117  efcj  12199  nninfctlemfo  12576  nn0seqcvgd  12578  algrp1  12583  alginv  12584  algcvg  12585  algcvga  12588  algfx  12589  eucalgcvga  12595  eulerthlem1  12764  eulerthlemh  12768  eulerthlemth  12769  pcmptcl  12880  pcmpt  12881  1arithlem4  12904  nninfdclemf1  13038  prdsplusgsgrpcl  13462  prdssgrpd  13463  prdsplusgcl  13494  prdsidlem  13495  prdsmndd  13496  gsumwsubmcl  13544  gsumwmhm  13546  grpinvcl  13596  prdsinvlem  13656  pwsinvg  13660  pwssub  13661  mhmmulg  13715  ghminv  13802  gsumfzreidx  13889  gsumfzsubmcl  13890  gsumfzmptfidmadd  13891  gsumfzmhm  13895  rhmdvdsr  14154  psrlinv  14663  psr1clfi  14667  mplsubgfilemcl  14678  cnptoprest2  14929  lmss  14935  txcnmpt  14962  txlm  14968  lmcn2  14969  psmetxrge0  15021  metcnp  15201  climcncf  15273  negfcncf  15295  ivthdec  15333  ivthreinc  15334  dvcnp2cntop  15388  dvaddxxbr  15390  dvimulf  15395  dvcj  15398  dvfre  15399  elply2  15424  plyaddlem1  15436  plymullem1  15437  plycolemc  15447  plyco  15448  dvply2g  15455  lgscllem  15701  lgsfle1  15703  lgsval4a  15716  lgsneg  15718  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  uhgrss  15890  uhgrm  15893  upgrss  15914  upgrm  15915  upgr1or2  15916  umgredg2en  15924  lfgredg2dom  15945  usgrss  15990  pw1map  16420  nninfall  16435  nninffeq  16446  refeq  16456  trilpolemclim  16464  trilpolemcl  16465  trilpolemisumle  16466  trilpolemeq1  16468  iswomni0  16479