Theorem ffvelcdmda 5728

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  ⟶wf 5276  ‘cfv 5280

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3003  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-id 4348  df-xp 4689  df-rel 4690  df-cnv 4691  df-co 4692  df-dm 4693  df-rn 4694  df-iota 5241  df-fun 5282  df-fn 5283  df-f 5284  df-fv 5288

This theorem is referenced by:  ffvelcdmd  5729  f1ocnvdm  5863  foeqcnvco  5872  f1oiso2  5909  offeq  6185  suppssof1  6189  ofco  6190  caofref  6196  caofinvl  6197  caofid0l  6198  caofid0r  6199  caofid1  6200  caofid2  6201  caofcom  6202  caofrss  6203  caoftrn  6204  caofdig  6205  smofvon2dm  6395  smofvon  6398  pw2f1odclem  6946  mapxpen  6960  xpmapenlem  6961  en2eqpr  7019  supisoex  7126  ordiso2  7152  omp1eomlem  7211  ctssdccl  7228  ctssdc  7230  enumctlemm  7231  enomnilem  7255  fodjuomnilemdc  7261  ismkvnex  7272  enmkvlem  7278  enwomnilem  7286  nninfwlporlemd  7289  nninfwlporlem  7290  nninfwlpoimlemginf  7293  cc3  7400  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgprlemladdrl  7811  caucvgprprlemopu  7832  caucvgprprlemexbt  7839  caucvgprprlemexb  7840  caucvgsrlemcl  7922  caucvgsrlemfv  7924  caucvgsrlemcau  7926  caucvgsrlembound  7927  caucvgsrlemoffval  7929  caucvgsrlemofff  7930  caucvgsrlemoffgt1  7932  caucvgsrlemoffres  7933  caucvgsr  7935  axcaucvglemcl  8028  ofnegsub  9055  frecuzrdgfunlem  10586  monoord2  10653  seq3f1o  10684  seqf1oglem2  10687  seqf1og  10688  seq3homo  10694  seqfeq3  10696  zfz1isolemiso  11006  seq3coll  11009  wrdsymbcl  11030  ccatcl  11072  resqrexlemfp1  11395  resqrexlemover  11396  resqrexlemdec  11397  resqrexlemlo  11399  resqrexlemcalc1  11400  resqrexlemcalc2  11401  resqrexlemcalc3  11402  resqrexlemgt0  11406  resqrexlemsqa  11410  clim2ser  11723  clim2ser2  11724  isermulc2  11726  iserle  11728  climserle  11731  climrecvg1n  11734  climcvg1nlem  11735  summodclem3  11766  summodclem2a  11767  fsumgcl  11772  fsum3  11773  fsumf1o  11776  isumss  11777  fisumss  11778  fsumcl2lem  11784  fsumadd  11792  isumclim3  11809  isummulc2  11812  isumrecl  11815  isumadd  11817  fsummulc2  11834  iserabs  11861  cvgcmpub  11862  isumshft  11876  isumsplit  11877  mertensabs  11923  clim2prod  11925  clim2divap  11926  prodfap0  11931  prodfdivap  11933  prodmodclem3  11961  prodmodclem2a  11962  fprodseq  11969  fprodf1o  11974  prodssdc  11975  fprodssdc  11976  fprodmul  11977  efcj  12059  nninfctlemfo  12436  nn0seqcvgd  12438  algrp1  12443  alginv  12444  algcvg  12445  algcvga  12448  algfx  12449  eucalgcvga  12455  eulerthlem1  12624  eulerthlemh  12628  eulerthlemth  12629  pcmptcl  12740  pcmpt  12741  1arithlem4  12764  nninfdclemf1  12898  prdsplusgsgrpcl  13321  prdssgrpd  13322  prdsplusgcl  13353  prdsidlem  13354  prdsmndd  13355  gsumwsubmcl  13403  gsumwmhm  13405  grpinvcl  13455  prdsinvlem  13515  pwsinvg  13519  pwssub  13520  mhmmulg  13574  ghminv  13661  gsumfzreidx  13748  gsumfzsubmcl  13749  gsumfzmptfidmadd  13750  gsumfzmhm  13754  rhmdvdsr  14012  psrlinv  14521  psr1clfi  14525  mplsubgfilemcl  14536  cnptoprest2  14787  lmss  14793  txcnmpt  14820  txlm  14826  lmcn2  14827  psmetxrge0  14879  metcnp  15059  climcncf  15131  negfcncf  15153  ivthdec  15191  ivthreinc  15192  dvcnp2cntop  15246  dvaddxxbr  15248  dvimulf  15253  dvcj  15256  dvfre  15257  elply2  15282  plyaddlem1  15294  plymullem1  15295  plycolemc  15305  plyco  15306  dvply2g  15313  lgscllem  15559  lgsfle1  15561  lgsval4a  15574  lgsneg  15576  lgsdir  15587  lgsdilem2  15588  lgsdi  15589  lgsne0  15590  uhgrss  15746  uhgrm  15749  upgrss  15770  upgrm  15771  upgr1or2  15772  umgredg2en  15780  pw1map  16073  nninfall  16087  nninffeq  16098  refeq  16108  trilpolemclim  16116  trilpolemcl  16117  trilpolemisumle  16118  trilpolemeq1  16120  iswomni0  16131