Theorem ffvelcdmda 5635

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2142  ⟶wf 5196  ‘cfv 5200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-sbc 2957  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-opab 4052  df-id 4279  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-fv 5208

This theorem is referenced by:  ffvelrnd  5636  f1ocnvdm  5764  foeqcnvco  5773  f1oiso2  5810  offeq  6078  suppssof1  6082  ofco  6083  caofref  6086  caofinvl  6087  caofcom  6088  caofrss  6089  caoftrn  6090  smofvon2dm  6279  smofvon  6282  mapxpen  6830  xpmapenlem  6831  en2eqpr  6889  supisoex  6990  ordiso2  7016  omp1eomlem  7075  ctssdccl  7092  ctssdc  7094  enumctlemm  7095  enomnilem  7118  fodjuomnilemdc  7124  ismkvnex  7135  enmkvlem  7141  enwomnilem  7149  nninfwlporlemd  7152  nninfwlporlem  7153  nninfwlpoimlemginf  7156  cc3  7234  cauappcvgprlemladdru  7622  cauappcvgprlemladdrl  7623  caucvgprlemladdrl  7644  caucvgprprlemopu  7665  caucvgprprlemexbt  7672  caucvgprprlemexb  7673  caucvgsrlemcl  7755  caucvgsrlemfv  7757  caucvgsrlemcau  7759  caucvgsrlembound  7760  caucvgsrlemoffval  7762  caucvgsrlemofff  7763  caucvgsrlemoffgt1  7765  caucvgsrlemoffres  7766  caucvgsr  7768  axcaucvglemcl  7861  frecuzrdgfunlem  10379  monoord2  10437  seq3f1o  10464  seq3homo  10470  seqfeq3  10472  zfz1isolemiso  10778  seq3coll  10781  resqrexlemfp1  10977  resqrexlemover  10978  resqrexlemdec  10979  resqrexlemlo  10981  resqrexlemcalc1  10982  resqrexlemcalc2  10983  resqrexlemcalc3  10984  resqrexlemgt0  10988  resqrexlemsqa  10992  clim2ser  11304  clim2ser2  11305  isermulc2  11307  iserle  11309  climserle  11312  climrecvg1n  11315  climcvg1nlem  11316  summodclem3  11347  summodclem2a  11348  fsumgcl  11353  fsum3  11354  fsumf1o  11357  isumss  11358  fisumss  11359  fsumcl2lem  11365  fsumadd  11373  isumclim3  11390  isummulc2  11393  isumrecl  11396  isumadd  11398  fsummulc2  11415  iserabs  11442  cvgcmpub  11443  isumshft  11457  isumsplit  11458  mertensabs  11504  clim2prod  11506  clim2divap  11507  prodfap0  11512  prodfdivap  11514  prodmodclem3  11542  prodmodclem2a  11543  fprodseq  11550  fprodf1o  11555  prodssdc  11556  fprodssdc  11557  fprodmul  11558  efcj  11640  nn0seqcvgd  11999  algrp1  12004  alginv  12005  algcvg  12006  algcvga  12009  algfx  12010  eucalgcvga  12016  eulerthlem1  12185  eulerthlemh  12189  eulerthlemth  12190  pcmptcl  12298  pcmpt  12299  1arithlem4  12322  nninfdclemf1  12411  grpinvcl  12773  mhmmulg  12874  cnptoprest2  13151  lmss  13157  txcnmpt  13184  txlm  13190  lmcn2  13191  psmetxrge0  13243  metcnp  13423  climcncf  13482  negfcncf  13500  ivthdec  13533  dvcnp2cntop  13574  dvaddxxbr  13576  dvimulf  13581  dvcj  13584  dvfre  13585  lgscllem  13819  lgsfle1  13821  lgsval4a  13834  lgsneg  13836  lgsdir  13847  lgsdilem2  13848  lgsdi  13849  lgsne0  13850  nninfall  14159  nninffeq  14170  refeq  14177  trilpolemclim  14185  trilpolemcl  14186  trilpolemisumle  14187  trilpolemeq1  14189  iswomni0  14200