Theorem ffvelcdmda 5769

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ⟶wf 5313  ‘cfv 5317

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-opab 4145  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-fv 5325

This theorem is referenced by:  ffvelcdmd  5770  f1ocnvdm  5904  foeqcnvco  5913  f1oiso2  5950  offeq  6230  suppssof1  6234  ofco  6235  caofref  6241  caofinvl  6242  caofid0l  6243  caofid0r  6244  caofid1  6245  caofid2  6246  caofcom  6247  caofrss  6248  caoftrn  6249  caofdig  6250  smofvon2dm  6440  smofvon  6443  pw2f1odclem  6991  mapxpen  7005  xpmapenlem  7006  en2eqpr  7065  supisoex  7172  ordiso2  7198  omp1eomlem  7257  ctssdccl  7274  ctssdc  7276  enumctlemm  7277  enomnilem  7301  fodjuomnilemdc  7307  ismkvnex  7318  enmkvlem  7324  enwomnilem  7332  nninfwlporlemd  7335  nninfwlporlem  7336  nninfwlpoimlemginf  7339  cc3  7450  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  caucvgprlemladdrl  7861  caucvgprprlemopu  7882  caucvgprprlemexbt  7889  caucvgprprlemexb  7890  caucvgsrlemcl  7972  caucvgsrlemfv  7974  caucvgsrlemcau  7976  caucvgsrlembound  7977  caucvgsrlemoffval  7979  caucvgsrlemofff  7980  caucvgsrlemoffgt1  7982  caucvgsrlemoffres  7983  caucvgsr  7985  axcaucvglemcl  8078  ofnegsub  9105  frecuzrdgfunlem  10636  monoord2  10703  seq3f1o  10734  seqf1oglem2  10737  seqf1og  10738  seq3homo  10744  seqfeq3  10746  zfz1isolemiso  11056  seq3coll  11059  wrdsymbcl  11080  ccatcl  11123  resqrexlemfp1  11515  resqrexlemover  11516  resqrexlemdec  11517  resqrexlemlo  11519  resqrexlemcalc1  11520  resqrexlemcalc2  11521  resqrexlemcalc3  11522  resqrexlemgt0  11526  resqrexlemsqa  11530  clim2ser  11843  clim2ser2  11844  isermulc2  11846  iserle  11848  climserle  11851  climrecvg1n  11854  climcvg1nlem  11855  summodclem3  11886  summodclem2a  11887  fsumgcl  11892  fsum3  11893  fsumf1o  11896  isumss  11897  fisumss  11898  fsumcl2lem  11904  fsumadd  11912  isumclim3  11929  isummulc2  11932  isumrecl  11935  isumadd  11937  fsummulc2  11954  iserabs  11981  cvgcmpub  11982  isumshft  11996  isumsplit  11997  mertensabs  12043  clim2prod  12045  clim2divap  12046  prodfap0  12051  prodfdivap  12053  prodmodclem3  12081  prodmodclem2a  12082  fprodseq  12089  fprodf1o  12094  prodssdc  12095  fprodssdc  12096  fprodmul  12097  efcj  12179  nninfctlemfo  12556  nn0seqcvgd  12558  algrp1  12563  alginv  12564  algcvg  12565  algcvga  12568  algfx  12569  eucalgcvga  12575  eulerthlem1  12744  eulerthlemh  12748  eulerthlemth  12749  pcmptcl  12860  pcmpt  12861  1arithlem4  12884  nninfdclemf1  13018  prdsplusgsgrpcl  13442  prdssgrpd  13443  prdsplusgcl  13474  prdsidlem  13475  prdsmndd  13476  gsumwsubmcl  13524  gsumwmhm  13526  grpinvcl  13576  prdsinvlem  13636  pwsinvg  13640  pwssub  13641  mhmmulg  13695  ghminv  13782  gsumfzreidx  13869  gsumfzsubmcl  13870  gsumfzmptfidmadd  13871  gsumfzmhm  13875  rhmdvdsr  14133  psrlinv  14642  psr1clfi  14646  mplsubgfilemcl  14657  cnptoprest2  14908  lmss  14914  txcnmpt  14941  txlm  14947  lmcn2  14948  psmetxrge0  15000  metcnp  15180  climcncf  15252  negfcncf  15274  ivthdec  15312  ivthreinc  15313  dvcnp2cntop  15367  dvaddxxbr  15369  dvimulf  15374  dvcj  15377  dvfre  15378  elply2  15403  plyaddlem1  15415  plymullem1  15416  plycolemc  15426  plyco  15427  dvply2g  15434  lgscllem  15680  lgsfle1  15682  lgsval4a  15695  lgsneg  15697  lgsdir  15708  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  uhgrss  15869  uhgrm  15872  upgrss  15893  upgrm  15894  upgr1or2  15895  umgredg2en  15903  lfgredg2dom  15924  usgrss  15969  pw1map  16320  nninfall  16334  nninffeq  16345  refeq  16355  trilpolemclim  16363  trilpolemcl  16364  trilpolemisumle  16365  trilpolemeq1  16367  iswomni0  16378