Theorem ffvelcdmda 5817

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ⟶wf 5353  ‘cfv 5357

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 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3046  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365

This theorem is referenced by:  ffvelcdmd  5818  f1ocnvdm  5960  foeqcnvco  5969  f1oiso2  6006  offeq  6289  suppssof1  6293  ofco  6294  caofref  6300  caofinvl  6301  caofid0l  6302  caofid0r  6303  caofid1  6304  caofid2  6305  caofcom  6306  caofrss  6307  caoftrn  6308  caofdig  6309  suppssrst  6474  suppssrgst  6475  suppofss1dcl  6477  suppofss2dcl  6478  smofvon2dm  6540  smofvon  6543  pw2f1odclem  7100  mapxpen  7114  xpmapenlem  7115  en2eqpr  7180  supisoex  7313  ordiso2  7339  omp1eomlem  7398  ctssdccl  7415  ctssdc  7417  enumctlemm  7418  enomnilem  7442  fodjuomnilemdc  7448  ismkvnex  7459  enmkvlem  7465  enwomnilem  7473  nninfwlporlemd  7476  nninfwlporlem  7477  nninfwlpoimlemginf  7480  cc3  7598  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprprlemopu  8030  caucvgprprlemexbt  8037  caucvgprprlemexb  8038  caucvgsrlemcl  8120  caucvgsrlemfv  8122  caucvgsrlemcau  8124  caucvgsrlembound  8125  caucvgsrlemoffval  8127  caucvgsrlemofff  8128  caucvgsrlemoffgt1  8130  caucvgsrlemoffres  8131  caucvgsr  8133  axcaucvglemcl  8226  ofnegsub  9253  frecuzrdgfunlem  10805  monoord2  10872  seq3f1o  10903  seqf1oglem2  10906  seqf1og  10907  seq3homo  10913  seqfeq3  10915  zfz1isolemiso  11236  seq3coll  11239  wrdsymbcl  11263  ccatcl  11306  resqrexlemfp1  11719  resqrexlemover  11720  resqrexlemdec  11721  resqrexlemlo  11723  resqrexlemcalc1  11724  resqrexlemcalc2  11725  resqrexlemcalc3  11726  resqrexlemgt0  11730  resqrexlemsqa  11734  clim2ser  12047  clim2ser2  12048  isermulc2  12050  iserle  12052  climserle  12055  climrecvg1n  12058  climcvg1nlem  12059  summodclem3  12091  summodclem2a  12092  fsumgcl  12097  fsum3  12098  fsumf1o  12101  isumss  12102  fisumss  12103  fsumcl2lem  12109  fsumadd  12117  isumclim3  12134  isummulc2  12137  isumrecl  12140  isumadd  12142  fsummulc2  12159  iserabs  12186  cvgcmpub  12187  isumshft  12201  isumsplit  12202  mertensabs  12248  clim2prod  12250  clim2divap  12251  prodfap0  12256  prodfdivap  12258  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  efcj  12384  nninfctlemfo  12761  nn0seqcvgd  12763  algrp1  12768  alginv  12769  algcvg  12770  algcvga  12773  algfx  12774  eucalgcvga  12780  eulerthlem1  12949  eulerthlemh  12953  eulerthlemth  12954  pcmptcl  13065  pcmpt  13066  1arithlem4  13089  nninfdclemf1  13287  gsumwsubmcl  13751  gsumwmhm  13753  grpinvcl  13803  mhmmulg  13916  ghminv  14003  gsumfzreidx  14090  gsumfzsubmcl  14091  gsumfzmptfidmadd  14092  gsumfzmhm  14096  prdsplusgsgrpcl  14132  prdssgrpd  14133  prdsplusgcl  14134  prdsidlem  14135  prdsmndd  14136  prdsinvlem  14138  pwsinvg  14157  pwssub  14158  rhmdvdsr  14420  rrgsupp  14512  psrbagcon  14952  psrbagconf1o  14954  psrlinv  14965  psr1clfi  14969  mplsubgfilemcl  14980  cnptoprest2  15231  lmss  15237  txcnmpt  15264  txlm  15270  lmcn2  15271  psmetxrge0  15323  metcnp  15503  climcncf  15575  negfcncf  15597  ivthdec  15635  ivthreinc  15636  dvcnp2cntop  15690  dvaddxxbr  15692  dvimulf  15697  dvcj  15700  dvfre  15701  elply2  15726  plyaddlem1  15738  plymullem1  15739  plycolemc  15749  plyco  15750  dvply2g  15757  lgscllem  16006  lgsfle1  16008  lgsval4a  16021  lgsneg  16023  lgsdir  16034  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  uhgrss  16196  uhgrm  16199  upgrss  16220  upgrm  16221  upgr1or2  16222  umgredg2en  16230  lfgredg2dom  16253  usgrss  16298  depindlem1  16627  depindlem2  16628  pw1map  16895  nninfall  16913  nninffeq  16924  refeq  16934  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  iswomni0  16962