Theorem ffvelcdmda 5778

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

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

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 4205  ax-pow 4262  ax-pr 4297

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 2802  df-sbc 3030  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-fv 5332

This theorem is referenced by:  ffvelcdmd  5779  f1ocnvdm  5917  foeqcnvco  5926  f1oiso2  5963  offeq  6244  suppssof1  6248  ofco  6249  caofref  6255  caofinvl  6256  caofid0l  6257  caofid0r  6258  caofid1  6259  caofid2  6260  caofcom  6261  caofrss  6262  caoftrn  6263  caofdig  6264  smofvon2dm  6457  smofvon  6460  pw2f1odclem  7015  mapxpen  7029  xpmapenlem  7030  en2eqpr  7092  supisoex  7199  ordiso2  7225  omp1eomlem  7284  ctssdccl  7301  ctssdc  7303  enumctlemm  7304  enomnilem  7328  fodjuomnilemdc  7334  ismkvnex  7345  enmkvlem  7351  enwomnilem  7359  nninfwlporlemd  7362  nninfwlporlem  7363  nninfwlpoimlemginf  7366  cc3  7477  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  caucvgprlemladdrl  7888  caucvgprprlemopu  7909  caucvgprprlemexbt  7916  caucvgprprlemexb  7917  caucvgsrlemcl  7999  caucvgsrlemfv  8001  caucvgsrlemcau  8003  caucvgsrlembound  8004  caucvgsrlemoffval  8006  caucvgsrlemofff  8007  caucvgsrlemoffgt1  8009  caucvgsrlemoffres  8010  caucvgsr  8012  axcaucvglemcl  8105  ofnegsub  9132  frecuzrdgfunlem  10671  monoord2  10738  seq3f1o  10769  seqf1oglem2  10772  seqf1og  10773  seq3homo  10779  seqfeq3  10781  zfz1isolemiso  11093  seq3coll  11096  wrdsymbcl  11117  ccatcl  11160  resqrexlemfp1  11560  resqrexlemover  11561  resqrexlemdec  11562  resqrexlemlo  11564  resqrexlemcalc1  11565  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemgt0  11571  resqrexlemsqa  11575  clim2ser  11888  clim2ser2  11889  isermulc2  11891  iserle  11893  climserle  11896  climrecvg1n  11899  climcvg1nlem  11900  summodclem3  11931  summodclem2a  11932  fsumgcl  11937  fsum3  11938  fsumf1o  11941  isumss  11942  fisumss  11943  fsumcl2lem  11949  fsumadd  11957  isumclim3  11974  isummulc2  11977  isumrecl  11980  isumadd  11982  fsummulc2  11999  iserabs  12026  cvgcmpub  12027  isumshft  12041  isumsplit  12042  mertensabs  12088  clim2prod  12090  clim2divap  12091  prodfap0  12096  prodfdivap  12098  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodmul  12142  efcj  12224  nninfctlemfo  12601  nn0seqcvgd  12603  algrp1  12608  alginv  12609  algcvg  12610  algcvga  12613  algfx  12614  eucalgcvga  12620  eulerthlem1  12789  eulerthlemh  12793  eulerthlemth  12794  pcmptcl  12905  pcmpt  12906  1arithlem4  12929  nninfdclemf1  13063  prdsplusgsgrpcl  13487  prdssgrpd  13488  prdsplusgcl  13519  prdsidlem  13520  prdsmndd  13521  gsumwsubmcl  13569  gsumwmhm  13571  grpinvcl  13621  prdsinvlem  13681  pwsinvg  13685  pwssub  13686  mhmmulg  13740  ghminv  13827  gsumfzreidx  13914  gsumfzsubmcl  13915  gsumfzmptfidmadd  13916  gsumfzmhm  13920  rhmdvdsr  14179  psrlinv  14688  psr1clfi  14692  mplsubgfilemcl  14703  cnptoprest2  14954  lmss  14960  txcnmpt  14987  txlm  14993  lmcn2  14994  psmetxrge0  15046  metcnp  15226  climcncf  15298  negfcncf  15320  ivthdec  15358  ivthreinc  15359  dvcnp2cntop  15413  dvaddxxbr  15415  dvimulf  15420  dvcj  15423  dvfre  15424  elply2  15449  plyaddlem1  15461  plymullem1  15462  plycolemc  15472  plyco  15473  dvply2g  15480  lgscllem  15726  lgsfle1  15728  lgsval4a  15741  lgsneg  15743  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  uhgrss  15916  uhgrm  15919  upgrss  15940  upgrm  15941  upgr1or2  15942  umgredg2en  15950  lfgredg2dom  15971  usgrss  16016  pw1map  16532  nninfall  16547  nninffeq  16558  refeq  16568  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  iswomni0  16591