Theorem ffvelcdmda 5790

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ⟶wf 5329  ‘cfv 5333

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 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-sbc 3033  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-fv 5341

This theorem is referenced by:  ffvelcdmd  5791  f1ocnvdm  5932  foeqcnvco  5941  f1oiso2  5978  offeq  6258  suppssof1  6262  ofco  6263  caofref  6269  caofinvl  6270  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  caofcom  6275  caofrss  6276  caoftrn  6277  caofdig  6278  suppssrst  6439  suppssrgst  6440  suppofss1dcl  6442  suppofss2dcl  6443  smofvon2dm  6505  smofvon  6508  pw2f1odclem  7063  mapxpen  7077  xpmapenlem  7078  en2eqpr  7142  supisoex  7251  ordiso2  7277  omp1eomlem  7336  ctssdccl  7353  ctssdc  7355  enumctlemm  7356  enomnilem  7380  fodjuomnilemdc  7386  ismkvnex  7397  enmkvlem  7403  enwomnilem  7411  nninfwlporlemd  7414  nninfwlporlem  7415  nninfwlpoimlemginf  7418  cc3  7530  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgprprlemopu  7962  caucvgprprlemexbt  7969  caucvgprprlemexb  7970  caucvgsrlemcl  8052  caucvgsrlemfv  8054  caucvgsrlemcau  8056  caucvgsrlembound  8057  caucvgsrlemoffval  8059  caucvgsrlemofff  8060  caucvgsrlemoffgt1  8062  caucvgsrlemoffres  8063  caucvgsr  8065  axcaucvglemcl  8158  ofnegsub  9184  frecuzrdgfunlem  10727  monoord2  10794  seq3f1o  10825  seqf1oglem2  10828  seqf1og  10829  seq3homo  10835  seqfeq3  10837  zfz1isolemiso  11149  seq3coll  11152  wrdsymbcl  11176  ccatcl  11219  resqrexlemfp1  11632  resqrexlemover  11633  resqrexlemdec  11634  resqrexlemlo  11636  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrexlemcalc3  11639  resqrexlemgt0  11643  resqrexlemsqa  11647  clim2ser  11960  clim2ser2  11961  isermulc2  11963  iserle  11965  climserle  11968  climrecvg1n  11971  climcvg1nlem  11972  summodclem3  12004  summodclem2a  12005  fsumgcl  12010  fsum3  12011  fsumf1o  12014  isumss  12015  fisumss  12016  fsumcl2lem  12022  fsumadd  12030  isumclim3  12047  isummulc2  12050  isumrecl  12053  isumadd  12055  fsummulc2  12072  iserabs  12099  cvgcmpub  12100  isumshft  12114  isumsplit  12115  mertensabs  12161  clim2prod  12163  clim2divap  12164  prodfap0  12169  prodfdivap  12171  prodmodclem3  12199  prodmodclem2a  12200  fprodseq  12207  fprodf1o  12212  prodssdc  12213  fprodssdc  12214  fprodmul  12215  efcj  12297  nninfctlemfo  12674  nn0seqcvgd  12676  algrp1  12681  alginv  12682  algcvg  12683  algcvga  12686  algfx  12687  eucalgcvga  12693  eulerthlem1  12862  eulerthlemh  12866  eulerthlemth  12867  pcmptcl  12978  pcmpt  12979  1arithlem4  13002  nninfdclemf1  13136  prdsplusgsgrpcl  13560  prdssgrpd  13561  prdsplusgcl  13592  prdsidlem  13593  prdsmndd  13594  gsumwsubmcl  13642  gsumwmhm  13644  grpinvcl  13694  prdsinvlem  13754  pwsinvg  13758  pwssub  13759  mhmmulg  13813  ghminv  13900  gsumfzreidx  13987  gsumfzsubmcl  13988  gsumfzmptfidmadd  13989  gsumfzmhm  13993  rhmdvdsr  14253  rrgsupp  14344  psrbagcon  14755  psrbagconf1o  14757  psrlinv  14768  psr1clfi  14772  mplsubgfilemcl  14783  cnptoprest2  15034  lmss  15040  txcnmpt  15067  txlm  15073  lmcn2  15074  psmetxrge0  15126  metcnp  15306  climcncf  15378  negfcncf  15400  ivthdec  15438  ivthreinc  15439  dvcnp2cntop  15493  dvaddxxbr  15495  dvimulf  15500  dvcj  15503  dvfre  15504  elply2  15529  plyaddlem1  15541  plymullem1  15542  plycolemc  15552  plyco  15553  dvply2g  15560  lgscllem  15809  lgsfle1  15811  lgsval4a  15824  lgsneg  15826  lgsdir  15837  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  uhgrss  15999  uhgrm  16002  upgrss  16023  upgrm  16024  upgr1or2  16025  umgredg2en  16033  lfgredg2dom  16056  usgrss  16101  depindlem1  16430  depindlem2  16431  pw1map  16700  nninfall  16718  nninffeq  16729  refeq  16739  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  iswomni0  16767