ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ffvelrnd Unicode version

Theorem ffvelrnd 5556
Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypotheses
Ref Expression
ffvelrnd.1  |-  ( ph  ->  F : A --> B )
ffvelrnd.2  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
ffvelrnd  |-  ( ph  ->  ( F `  C
)  e.  B )

Proof of Theorem ffvelrnd
StepHypRef Expression
1 ffvelrnd.2 . 2  |-  ( ph  ->  C  e.  A )
2 ffvelrnd.1 . . 3  |-  ( ph  ->  F : A --> B )
32ffvelrnda 5555 . 2  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
41, 3mpdan 417 1  |-  ( ph  ->  ( F `  C
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480   -->wf 5119   ` cfv 5123
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-sbc 2910  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-fv 5131
This theorem is referenced by:  isotr  5717  caofinvl  6004  rdgon  6283  frecabcl  6296  phplem4dom  6756  fidceq  6763  dif1en  6773  fin0  6779  fin0or  6780  infm  6798  en2eqpr  6801  fidcenumlemrks  6841  fidcenumlemr  6843  supisoti  6897  ordiso2  6920  updjudhcoinlf  6965  updjudhcoinrg  6966  caseinl  6976  caseinr  6977  difinfsnlem  6984  difinfsn  6985  ctmlemr  6993  ctssdclemn0  6995  ctssdc  6998  enumctlemm  6999  enumct  7000  enomnilem  7010  finomni  7012  ismkvnex  7029  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  cauappcvgprlemm  7460  cauappcvgprlemdisj  7466  cauappcvgprlemloc  7467  cauappcvgprlemladdfu  7469  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  cauappcvgprlem1  7474  cauappcvgprlem2  7475  caucvgprlemnkj  7481  caucvgprlemnbj  7482  caucvgprlemm  7483  caucvgprlemloc  7490  caucvgprlemladdfu  7492  caucvgprlemladdrl  7493  caucvgprlem1  7494  caucvgprlem2  7495  caucvgprprlemnkltj  7504  caucvgprprlemnkeqj  7505  caucvgprprlemnbj  7508  caucvgprprlemmu  7510  caucvgprprlemopl  7512  caucvgprprlemloc  7518  caucvgprprlemexbt  7521  caucvgprprlemexb  7522  caucvgprprlemaddq  7523  caucvgprprlem1  7524  caucvgprprlem2  7525  caucvgsrlemcau  7608  caucvgsrlemgt1  7610  caucvgsrlemoffcau  7613  caucvgsrlemoffres  7615  caucvgsr  7617  axcaucvglemval  7712  axcaucvglemcau  7713  axcaucvglemres  7714  fseq1p1m1  9881  4fvwrd4  9924  fvinim0ffz  10025  frecuzrdgg  10196  frecuzrdgsuctlem  10203  seq3val  10238  seqvalcd  10239  seq3p1  10242  seqp1cd  10246  ser3mono  10258  seq3split  10259  seq3caopr2  10262  iseqf1olemkle  10264  iseqf1olemklt  10265  iseqf1olemqcl  10266  iseqf1olemnab  10268  iseqf1olemmo  10272  iseqf1olemqk  10274  iseqf1olemjpcl  10275  iseqf1olemqpcl  10276  iseqf1olemfvp  10277  seq3f1olemqsumkj  10278  seq3f1olemqsumk  10279  seq3f1olemqsum  10280  seq3f1olemstep  10281  seq3f1oleml  10283  seq3f1o  10284  seq3z  10291  seq3distr  10293  ser3ge0  10297  ser3le  10298  exp3vallem  10301  exp3val  10302  bcval5  10516  hashfz1  10536  resunimafz0  10581  leisorel  10587  zfz1isolemiso  10589  seq3coll  10592  caucvgrelemcau  10759  caucvgre  10760  cvg1nlemf  10762  cvg1nlemcau  10763  cvg1nlemres  10764  recvguniqlem  10773  resqrexlemdecn  10791  resqrexlemcalc3  10795  resqrexlemnmsq  10796  resqrexlemnm  10797  resqrexlemcvg  10798  resqrexlemoverl  10800  resqrexlemglsq  10801  resqrexlemga  10802  clim2ser  11113  clim2ser2  11114  climrecvg1n  11124  climcvg1nlem  11125  serf0  11128  sumeq2  11135  fsum3cvg  11154  summodclem2a  11157  fsum3  11163  fisumss  11168  fsumcl2lem  11174  fsumadd  11182  fsummulc2  11224  fsumrelem  11247  isumshft  11266  cvgratnnlemseq  11302  cvgratnnlemrate  11306  clim2prod  11315  clim2divap  11316  prodfrecap  11322  prodfdivap  11323  ntrivcvgap  11324  prodeq2  11333  fproddccvg  11348  prodmodclem3  11351  prodmodclem2a  11352  effsumlt  11405  nn0seqcvgd  11729  ialgrlem1st  11730  ennnfonelemdc  11919  ennnfonelemjn  11922  ennnfonelemg  11923  ennnfonelemp1  11926  ennnfonelemom  11928  ennnfonelemhdmp1  11929  ennnfonelemss  11930  ennnfonelemkh  11932  ennnfonelemhf1o  11933  ennnfonelemex  11934  ennnfonelemhom  11935  ennnfonelemnn0  11942  ennnfonelemim  11944  ctinfomlemom  11947  ctiunctlemudc  11957  ctiunctlemf  11958  ctiunctlemfo  11959  iscnp4  12397  cnptopco  12401  lmtopcnp  12429  upxp  12451  uptx  12453  txlm  12458  comet  12678  metcnp3  12690  metcnp  12691  metcnp2  12692  metcnpi3  12696  elcncf2  12740  cncfco  12757  limcimolemlt  12812  cnplimcim  12815  cnplimclemle  12816  cnplimclemr  12817  limccnpcntop  12823  dvlemap  12828  dvcnp2cntop  12842  dvaddxxbr  12844  dvmulxxbr  12845  dvcoapbr  12850  dvcjbr  12851  dvef  12866  pwle2  13223  subctctexmid  13226  nnsf  13229  peano4nninf  13230  nninfalllem1  13233  nninfsellemdc  13236  nninfsellemeq  13240  nninfsellemqall  13241  nninfsellemeqinf  13242  nninfomnilem  13244  isomninnlem  13255  trilpolemeq1  13263  trilpolemlt1  13264
  Copyright terms: Public domain W3C validator