Theorem ffvelcdmda 5843

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ⟶wf 5373  ‘cfv 5377

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 4249  ax-pow 4311  ax-pr 4346

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 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385

This theorem is used by:  ffvelcdmd  5844  f1ocnvdm  5987  foeqcnvco  5996  f1oiso2  6033  offeq  6316  suppssof1  6320  ofco  6321  caofref  6327  caofinvl  6328  caofid0l  6329  caofid0r  6330  caofid1  6331  caofid2  6332  caofcom  6333  caofrss  6334  caoftrn  6335  caofdig  6336  suppssrst  6501  suppssrgst  6502  suppofss1dcl  6504  suppofss2dcl  6505  smofvon2dm  6567  smofvon  6570  pw2f1odclem  7134  mapxpen  7148  xpmapenlem  7149  en2eqpr  7214  supisoex  7349  ordiso2  7375  omp1eomlem  7434  ctssdccl  7451  ctssdc  7453  enumctlemm  7454  enomnilem  7478  fodjuomnilemdc  7484  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  nninfwlporlemd  7512  nninfwlporlem  7513  nninfwlpoimlemginf  7516  cc3  7634  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgprprlemopu  8066  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  caucvgsrlemcl  8156  caucvgsrlemfv  8158  caucvgsrlemcau  8160  caucvgsrlembound  8161  caucvgsrlemoffval  8163  caucvgsrlemofff  8164  caucvgsrlemoffgt1  8166  caucvgsrlemoffres  8167  caucvgsr  8169  axcaucvglemcl  8262  ofnegsub  9294  frecuzrdgfunlem  10869  monoord2  10936  seq3f1o  10967  seqf1oglem2  10970  seqf1og  10971  seq3homo  10977  seqfeq3  10979  zfz1isolemiso  11305  seq3coll  11308  wrdsymbcl  11332  ccatcl  11375  resqrexlemfp1  11789  resqrexlemover  11790  resqrexlemdec  11791  resqrexlemlo  11793  resqrexlemcalc1  11794  resqrexlemcalc2  11795  resqrexlemcalc3  11796  resqrexlemgt0  11800  resqrexlemsqa  11804  clim2ser  12119  clim2ser2  12120  isermulc2  12122  iserle  12124  climserle  12127  climrecvg1n  12130  climcvg1nlem  12131  summodclem3  12163  summodclem2a  12164  fsumgcl  12169  fsum3  12170  fsumf1o  12173  isumss  12174  fisumss  12175  fsumcl2lem  12181  fsumadd  12189  isumclim3  12206  isummulc2  12209  isumrecl  12212  isumadd  12214  fsummulc2  12231  iserabs  12258  cvgcmpub  12259  isumshft  12273  isumsplit  12274  mertensabs  12320  clim2prod  12322  clim2divap  12323  prodfap0  12328  prodfdivap  12330  prodmodclem3  12358  prodmodclem2a  12359  fprodseq  12366  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodmul  12374  efcj  12456  nninfctlemfo  12833  nn0seqcvgd  12835  algrp1  12840  alginv  12841  algcvg  12842  algcvga  12845  algfx  12846  eucalgcvga  12852  eulerthlem1  13025  eulerthlemh  13029  eulerthlemth  13030  pcmptcl  13141  pcmpt  13142  1arithlem4  13165  nninfdclemf1  13392  gzsumwsubmcl  13850  gzsumwmhm  13852  grpinvcl  13902  mhmmulg  14015  ghminv  14102  gzsumreidx  14190  gzsumsubmcl  14191  gzsummhm  14194  gsumf1ofi  14209  prdsplusgsgrpcl  14239  prdssgrpd  14240  prdsplusgcl  14241  prdsidlem  14242  prdsmndd  14243  prdsinvlem  14245  pwsinvg  14264  pwssub  14265  rhmdvdsr  14531  rrgsupp  14623  ascldimul  15080  psrbagcon  15111  psrbagconf1o  15113  psrlinv  15124  psr1clfi  15128  mplsubgfilemcl  15139  cnptoprest2  15390  lmss  15396  txcnmpt  15423  txlm  15429  lmcn2  15430  psmetxrge0  15482  metcnp  15662  climcncf  15734  negfcncf  15756  ivthdec  15794  ivthreinc  15795  dvcnp2cntop  15849  dvaddxxbr  15851  dvimulf  15856  dvcj  15859  dvfre  15860  elply2  15885  plyaddlem1  15897  plymullem1  15898  plycolemc  15908  plyco  15909  dvply2g  15916  bposlem5  16213  lgscllem  16224  lgsfle1  16226  lgsval4a  16239  lgsneg  16241  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  uhgrss  16414  uhgrm  16417  upgrss  16438  upgrm  16439  upgr1or2  16440  umgredg2en  16448  lfgredg2dom  16471  usgrss  16516  depindlem1  16845  depindlem2  16846  pw1map  17123  nninfall  17150  nninffeq  17161  refeq  17171  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  iswomni0  17199