Theorem ffvelcdmda 5653

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  ⟶wf 5214  ‘cfv 5218

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-sbc 2965  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-fv 5226

This theorem is referenced by:  ffvelcdmd  5654  f1ocnvdm  5784  foeqcnvco  5793  f1oiso2  5830  offeq  6098  suppssof1  6102  ofco  6103  caofref  6106  caofinvl  6107  caofcom  6108  caofrss  6109  caoftrn  6110  smofvon2dm  6299  smofvon  6302  mapxpen  6850  xpmapenlem  6851  en2eqpr  6909  supisoex  7010  ordiso2  7036  omp1eomlem  7095  ctssdccl  7112  ctssdc  7114  enumctlemm  7115  enomnilem  7138  fodjuomnilemdc  7144  ismkvnex  7155  enmkvlem  7161  enwomnilem  7169  nninfwlporlemd  7172  nninfwlporlem  7173  nninfwlpoimlemginf  7176  cc3  7269  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemladdrl  7679  caucvgprprlemopu  7700  caucvgprprlemexbt  7707  caucvgprprlemexb  7708  caucvgsrlemcl  7790  caucvgsrlemfv  7792  caucvgsrlemcau  7794  caucvgsrlembound  7795  caucvgsrlemoffval  7797  caucvgsrlemofff  7798  caucvgsrlemoffgt1  7800  caucvgsrlemoffres  7801  caucvgsr  7803  axcaucvglemcl  7896  frecuzrdgfunlem  10421  monoord2  10479  seq3f1o  10506  seq3homo  10512  seqfeq3  10514  zfz1isolemiso  10821  seq3coll  10824  resqrexlemfp1  11020  resqrexlemover  11021  resqrexlemdec  11022  resqrexlemlo  11024  resqrexlemcalc1  11025  resqrexlemcalc2  11026  resqrexlemcalc3  11027  resqrexlemgt0  11031  resqrexlemsqa  11035  clim2ser  11347  clim2ser2  11348  isermulc2  11350  iserle  11352  climserle  11355  climrecvg1n  11358  climcvg1nlem  11359  summodclem3  11390  summodclem2a  11391  fsumgcl  11396  fsum3  11397  fsumf1o  11400  isumss  11401  fisumss  11402  fsumcl2lem  11408  fsumadd  11416  isumclim3  11433  isummulc2  11436  isumrecl  11439  isumadd  11441  fsummulc2  11458  iserabs  11485  cvgcmpub  11486  isumshft  11500  isumsplit  11501  mertensabs  11547  clim2prod  11549  clim2divap  11550  prodfap0  11555  prodfdivap  11557  prodmodclem3  11585  prodmodclem2a  11586  fprodseq  11593  fprodf1o  11598  prodssdc  11599  fprodssdc  11600  fprodmul  11601  efcj  11683  nn0seqcvgd  12043  algrp1  12048  alginv  12049  algcvg  12050  algcvga  12053  algfx  12054  eucalgcvga  12060  eulerthlem1  12229  eulerthlemh  12233  eulerthlemth  12234  pcmptcl  12342  pcmpt  12343  1arithlem4  12366  nninfdclemf1  12455  grpinvcl  12926  mhmmulg  13029  cnptoprest2  13779  lmss  13785  txcnmpt  13812  txlm  13818  lmcn2  13819  psmetxrge0  13871  metcnp  14051  climcncf  14110  negfcncf  14128  ivthdec  14161  dvcnp2cntop  14202  dvaddxxbr  14204  dvimulf  14209  dvcj  14212  dvfre  14213  lgscllem  14447  lgsfle1  14449  lgsval4a  14462  lgsneg  14464  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  nninfall  14797  nninffeq  14808  refeq  14815  trilpolemclim  14823  trilpolemcl  14824  trilpolemisumle  14825  trilpolemeq1  14827  iswomni0  14838