Theorem ffvelcdmda 5846

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

Hypothesis

Ref	Expression
ffvelcdmd.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
ffvelcdmda	|- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Proof of Theorem ffvelcdmda

Step	Hyp	Ref	Expression
1		ffvelcdmd.1	. 2 |- ( ph -> F : A --> B )
2		ffvelcdm 5844	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3	1, 2	sylan 283	1 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   -->wf 5376   ` cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388

This theorem is used by:  ffvelcdmd  5847  f1ocnvdm  5990  foeqcnvco  5999  f1oiso2  6036  offeq  6320  suppssof1  6324  ofco  6325  caofref  6331  caofinvl  6332  caofid0l  6333  caofid0r  6334  caofid1  6335  caofid2  6336  caofcom  6337  caofrss  6338  caoftrn  6339  caofdig  6340  suppssrst  6505  suppssrgst  6506  suppofss1dcl  6508  suppofss2dcl  6509  suppinisegdc  6513  smofvon2dm  6572  smofvon  6575  pw2f1odclem  7140  mapxpen  7154  xpmapenlem  7155  en2eqpr  7220  supisoex  7355  ordiso2  7381  omp1eomlem  7440  ctssdccl  7457  ctssdc  7459  enumctlemm  7460  enomnilem  7484  fodjuomnilemdc  7490  ismkvnex  7501  enmkvlem  7507  enwomnilem  7515  nninfwlporlemd  7518  nninfwlporlem  7519  nninfwlpoimlemginf  7522  cc3  7640  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdrl  8051  caucvgprprlemopu  8072  caucvgprprlemexbt  8079  caucvgprprlemexb  8080  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsrlemcau  8166  caucvgsrlembound  8167  caucvgsrlemoffval  8169  caucvgsrlemofff  8170  caucvgsrlemoffgt1  8172  caucvgsrlemoffres  8173  caucvgsr  8175  axcaucvglemcl  8268  ofsubeq0  9300  ofnegsub  9301  frecuzrdgfunlem  10876  monoord2  10943  seq3f1o  10974  seqf1oglem2  10977  seqf1og  10978  seq3homo  10984  seqfeq3  10986  zfz1isolemiso  11312  seq3coll  11315  wrdsymbcl  11339  ccatcl  11382  resqrexlemfp1  11796  resqrexlemover  11797  resqrexlemdec  11798  resqrexlemlo  11800  resqrexlemcalc1  11801  resqrexlemcalc2  11802  resqrexlemcalc3  11803  resqrexlemgt0  11807  resqrexlemsqa  11811  clim2ser  12127  clim2ser2  12128  isermulc2  12130  iserle  12132  climserle  12135  climrecvg1n  12138  climcvg1nlem  12139  summodclem3  12171  summodclem2a  12172  fsumgcl  12177  fsum3  12178  fsumf1o  12181  isumss  12182  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  isumclim3  12214  isummulc2  12217  isumrecl  12220  isumadd  12222  fsummulc2  12239  iserabs  12266  cvgcmpub  12267  isumshft  12281  isumsplit  12282  mertensabs  12328  clim2prod  12330  clim2divap  12331  prodfap0  12336  prodfdivap  12338  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodmul  12382  efcj  12464  nninfctlemfo  12841  nn0seqcvgd  12843  algrp1  12848  alginv  12849  algcvg  12850  algcvga  12853  algfx  12854  eucalgcvga  12860  eulerthlem1  13033  eulerthlemh  13037  eulerthlemth  13038  pcmptcl  13149  pcmpt  13150  1arithlem4  13173  nninfdclemf1  13400  gzsumwsubmcl  13859  gzsumwmhm  13861  grpinvcl  13911  mhmmulg  14024  ghminv  14111  gzsumreidx  14230  gzsumsubmcl  14231  gzsummhm  14234  gsumf1ofi  14249  gsumsplitfi  14255  gsum2dfilem1  14270  gsum2dfilem2  14271  prdsplusgsgrpcl  14296  prdssgrpd  14297  prdsplusgcl  14298  prdsidlem  14299  prdsmndd  14300  prdsinvlem  14302  pwsinvg  14321  pwssub  14322  rhmdvdsr  14590  rrgsupp  14682  ascldimul  15139  psrbagdceq  15167  psrbagcon  15174  psrbaglefifi  15175  psrbagconf1o  15177  psrbagmaxlem1a  15179  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  gsumbagdiaglem  15184  psrass1filem  15186  psrlinv  15203  psr1clfi  15207  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  psrdifi  15211  psrdirfi  15212  mplsubgfilemcl  15232  cnptoprest2  15483  lmss  15489  txcnmpt  15516  txlm  15522  lmcn2  15523  psmetxrge0  15575  metcnp  15755  climcncf  15827  negfcncf  15849  ivthdec  15887  ivthreinc  15888  dvcnp2cntop  15942  dvaddxxbr  15944  dvimulf  15949  dvcj  15952  dvfre  15953  elply2  15978  plyaddlem1  15990  plymullem1  15991  plycolemc  16001  plyco  16002  dvply2g  16009  bposlem5  16332  lgscllem  16348  lgsfle1  16350  lgsval4a  16363  lgsneg  16365  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  uhgrss  16538  uhgrm  16541  upgrss  16562  upgrm  16563  upgr1or2  16564  umgredg2en  16572  lfgredg2dom  16595  usgrss  16640  depindlem1  16969  depindlem2  16970  pw1map  17247  nninfall  17275  nninffeq  17286  refeq  17296  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  iswomni0  17325