Theorem ffvelcdmda 5782

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ⟶wf 5322  ‘cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334

This theorem is referenced by:  ffvelcdmd  5783  f1ocnvdm  5921  foeqcnvco  5930  f1oiso2  5967  offeq  6248  suppssof1  6252  ofco  6253  caofref  6259  caofinvl  6260  caofid0l  6261  caofid0r  6262  caofid1  6263  caofid2  6264  caofcom  6265  caofrss  6266  caoftrn  6267  caofdig  6268  smofvon2dm  6461  smofvon  6464  pw2f1odclem  7019  mapxpen  7033  xpmapenlem  7034  en2eqpr  7098  supisoex  7207  ordiso2  7233  omp1eomlem  7292  ctssdccl  7309  ctssdc  7311  enumctlemm  7312  enomnilem  7336  fodjuomnilemdc  7342  ismkvnex  7353  enmkvlem  7359  enwomnilem  7367  nninfwlporlemd  7370  nninfwlporlem  7371  nninfwlpoimlemginf  7374  cc3  7486  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  caucvgprlemladdrl  7897  caucvgprprlemopu  7918  caucvgprprlemexbt  7925  caucvgprprlemexb  7926  caucvgsrlemcl  8008  caucvgsrlemfv  8010  caucvgsrlemcau  8012  caucvgsrlembound  8013  caucvgsrlemoffval  8015  caucvgsrlemofff  8016  caucvgsrlemoffgt1  8018  caucvgsrlemoffres  8019  caucvgsr  8021  axcaucvglemcl  8114  ofnegsub  9141  frecuzrdgfunlem  10680  monoord2  10747  seq3f1o  10778  seqf1oglem2  10781  seqf1og  10782  seq3homo  10788  seqfeq3  10790  zfz1isolemiso  11102  seq3coll  11105  wrdsymbcl  11126  ccatcl  11169  resqrexlemfp1  11569  resqrexlemover  11570  resqrexlemdec  11571  resqrexlemlo  11573  resqrexlemcalc1  11574  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemgt0  11580  resqrexlemsqa  11584  clim2ser  11897  clim2ser2  11898  isermulc2  11900  iserle  11902  climserle  11905  climrecvg1n  11908  climcvg1nlem  11909  summodclem3  11940  summodclem2a  11941  fsumgcl  11946  fsum3  11947  fsumf1o  11950  isumss  11951  fisumss  11952  fsumcl2lem  11958  fsumadd  11966  isumclim3  11983  isummulc2  11986  isumrecl  11989  isumadd  11991  fsummulc2  12008  iserabs  12035  cvgcmpub  12036  isumshft  12050  isumsplit  12051  mertensabs  12097  clim2prod  12099  clim2divap  12100  prodfap0  12105  prodfdivap  12107  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodmul  12151  efcj  12233  nninfctlemfo  12610  nn0seqcvgd  12612  algrp1  12617  alginv  12618  algcvg  12619  algcvga  12622  algfx  12623  eucalgcvga  12629  eulerthlem1  12798  eulerthlemh  12802  eulerthlemth  12803  pcmptcl  12914  pcmpt  12915  1arithlem4  12938  nninfdclemf1  13072  prdsplusgsgrpcl  13496  prdssgrpd  13497  prdsplusgcl  13528  prdsidlem  13529  prdsmndd  13530  gsumwsubmcl  13578  gsumwmhm  13580  grpinvcl  13630  prdsinvlem  13690  pwsinvg  13694  pwssub  13695  mhmmulg  13749  ghminv  13836  gsumfzreidx  13923  gsumfzsubmcl  13924  gsumfzmptfidmadd  13925  gsumfzmhm  13929  rhmdvdsr  14188  psrlinv  14697  psr1clfi  14701  mplsubgfilemcl  14712  cnptoprest2  14963  lmss  14969  txcnmpt  14996  txlm  15002  lmcn2  15003  psmetxrge0  15055  metcnp  15235  climcncf  15307  negfcncf  15329  ivthdec  15367  ivthreinc  15368  dvcnp2cntop  15422  dvaddxxbr  15424  dvimulf  15429  dvcj  15432  dvfre  15433  elply2  15458  plyaddlem1  15470  plymullem1  15471  plycolemc  15481  plyco  15482  dvply2g  15489  lgscllem  15735  lgsfle1  15737  lgsval4a  15750  lgsneg  15752  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  uhgrss  15925  uhgrm  15928  upgrss  15949  upgrm  15950  upgr1or2  15951  umgredg2en  15959  lfgredg2dom  15982  usgrss  16027  pw1map  16596  nninfall  16611  nninffeq  16622  refeq  16632  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  iswomni0  16655