Theorem ffvelcdmda 5700

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  ⟶wf 5255  ‘cfv 5259

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-sbc 2990  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-opab 4096  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-fv 5267

This theorem is referenced by:  ffvelcdmd  5701  f1ocnvdm  5831  foeqcnvco  5840  f1oiso2  5877  offeq  6153  suppssof1  6157  ofco  6158  caofref  6163  caofinvl  6164  caofcom  6165  caofrss  6166  caoftrn  6167  caofdig  6168  smofvon2dm  6358  smofvon  6361  pw2f1odclem  6899  mapxpen  6913  xpmapenlem  6914  en2eqpr  6972  supisoex  7079  ordiso2  7105  omp1eomlem  7164  ctssdccl  7181  ctssdc  7183  enumctlemm  7184  enomnilem  7208  fodjuomnilemdc  7214  ismkvnex  7225  enmkvlem  7231  enwomnilem  7239  nninfwlporlemd  7242  nninfwlporlem  7243  nninfwlpoimlemginf  7246  cc3  7340  cauappcvgprlemladdru  7728  cauappcvgprlemladdrl  7729  caucvgprlemladdrl  7750  caucvgprprlemopu  7771  caucvgprprlemexbt  7778  caucvgprprlemexb  7779  caucvgsrlemcl  7861  caucvgsrlemfv  7863  caucvgsrlemcau  7865  caucvgsrlembound  7866  caucvgsrlemoffval  7868  caucvgsrlemofff  7869  caucvgsrlemoffgt1  7871  caucvgsrlemoffres  7872  caucvgsr  7874  axcaucvglemcl  7967  ofnegsub  8994  frecuzrdgfunlem  10516  monoord2  10583  seq3f1o  10614  seqf1oglem2  10617  seqf1og  10618  seq3homo  10624  seqfeq3  10626  zfz1isolemiso  10936  seq3coll  10939  wrdsymbcl  10954  resqrexlemfp1  11179  resqrexlemover  11180  resqrexlemdec  11181  resqrexlemlo  11183  resqrexlemcalc1  11184  resqrexlemcalc2  11185  resqrexlemcalc3  11186  resqrexlemgt0  11190  resqrexlemsqa  11194  clim2ser  11507  clim2ser2  11508  isermulc2  11510  iserle  11512  climserle  11515  climrecvg1n  11518  climcvg1nlem  11519  summodclem3  11550  summodclem2a  11551  fsumgcl  11556  fsum3  11557  fsumf1o  11560  isumss  11561  fisumss  11562  fsumcl2lem  11568  fsumadd  11576  isumclim3  11593  isummulc2  11596  isumrecl  11599  isumadd  11601  fsummulc2  11618  iserabs  11645  cvgcmpub  11646  isumshft  11660  isumsplit  11661  mertensabs  11707  clim2prod  11709  clim2divap  11710  prodfap0  11715  prodfdivap  11717  prodmodclem3  11745  prodmodclem2a  11746  fprodseq  11753  fprodf1o  11758  prodssdc  11759  fprodssdc  11760  fprodmul  11761  efcj  11843  nninfctlemfo  12220  nn0seqcvgd  12222  algrp1  12227  alginv  12228  algcvg  12229  algcvga  12232  algfx  12233  eucalgcvga  12239  eulerthlem1  12408  eulerthlemh  12412  eulerthlemth  12413  pcmptcl  12524  pcmpt  12525  1arithlem4  12548  nninfdclemf1  12682  gsumwsubmcl  13175  gsumwmhm  13177  grpinvcl  13227  mhmmulg  13340  ghminv  13427  gsumfzreidx  13514  gsumfzsubmcl  13515  gsumfzmptfidmadd  13516  gsumfzmhm  13520  rhmdvdsr  13778  cnptoprest2  14523  lmss  14529  txcnmpt  14556  txlm  14562  lmcn2  14563  psmetxrge0  14615  metcnp  14795  climcncf  14867  negfcncf  14889  ivthdec  14927  ivthreinc  14928  dvcnp2cntop  14982  dvaddxxbr  14984  dvimulf  14989  dvcj  14992  dvfre  14993  elply2  15018  plyaddlem1  15030  plymullem1  15031  plycolemc  15041  plyco  15042  dvply2g  15049  lgscllem  15295  lgsfle1  15297  lgsval4a  15310  lgsneg  15312  lgsdir  15323  lgsdilem2  15324  lgsdi  15325  lgsne0  15326  nninfall  15703  nninffeq  15714  refeq  15722  trilpolemclim  15730  trilpolemcl  15731  trilpolemisumle  15732  trilpolemeq1  15734  iswomni0  15745