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

Theorem ffvelrnd 5435
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 5434 . 2  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
41, 3mpdan 412 1  |-  ( ph  ->  ( F `  C
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   -->wf 5011   ` cfv 5015
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-sbc 2841  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-br 3846  df-opab 3900  df-id 4120  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-fv 5023
This theorem is referenced by:  isotr  5595  caofinvl  5877  rdgon  6151  frecabcl  6164  phplem4dom  6578  fidceq  6585  dif1en  6595  fin0  6601  fin0or  6602  infm  6620  en2eqpr  6623  fidcenumlemrks  6662  fidcenumlemr  6664  supisoti  6705  ordiso2  6728  updjudhcoinlf  6771  updjudhcoinrg  6772  enomnilem  6794  finomni  6796  exmidfodomrlemr  6828  exmidfodomrlemrALT  6829  cauappcvgprlemm  7204  cauappcvgprlemdisj  7210  cauappcvgprlemloc  7211  cauappcvgprlemladdfu  7213  cauappcvgprlemladdru  7215  cauappcvgprlemladdrl  7216  cauappcvgprlem1  7218  cauappcvgprlem2  7219  caucvgprlemnkj  7225  caucvgprlemnbj  7226  caucvgprlemm  7227  caucvgprlemloc  7234  caucvgprlemladdfu  7236  caucvgprlemladdrl  7237  caucvgprlem1  7238  caucvgprlem2  7239  caucvgprprlemnkltj  7248  caucvgprprlemnkeqj  7249  caucvgprprlemnbj  7252  caucvgprprlemmu  7254  caucvgprprlemopl  7256  caucvgprprlemloc  7262  caucvgprprlemexbt  7265  caucvgprprlemexb  7266  caucvgprprlemaddq  7267  caucvgprprlem1  7268  caucvgprprlem2  7269  caucvgsrlemcau  7338  caucvgsrlemgt1  7340  caucvgsrlemoffcau  7343  caucvgsrlemoffres  7345  caucvgsr  7347  axcaucvglemval  7432  axcaucvglemcau  7433  axcaucvglemres  7434  fseq1p1m1  9508  4fvwrd4  9551  fvinim0ffz  9652  frecuzrdgg  9823  frecuzrdgsuctlem  9830  iseqvalt  9873  seq3val  9874  iseqcl  9881  iseqp1t  9883  seq3p1  9884  seq3split  9907  iseqf1olemkle  9913  iseqf1olemklt  9914  iseqf1olemqcl  9915  iseqf1olemnab  9917  iseqf1olemmo  9921  iseqf1olemqk  9923  iseqf1olemjpcl  9924  iseqf1olemqpcl  9925  iseqf1olemfvp  9926  seq3f1olemqsumkj  9927  seq3f1olemqsumk  9928  seq3f1olemqsum  9929  seq3f1olemstep  9930  seq3f1oleml  9932  seq3f1o  9933  seq3distr  9946  ser3ge0  9952  ser3le  9953  exp3vallem  9956  exp3val  9957  hashfz1  10191  resunimafz0  10236  leisorel  10242  zfz1isolemiso  10244  iseqcoll  10247  caucvgrelemcau  10413  caucvgre  10414  cvg1nlemf  10416  cvg1nlemcau  10417  cvg1nlemres  10418  recvguniqlem  10427  resqrexlemdecn  10445  resqrexlemcalc3  10449  resqrexlemnmsq  10450  resqrexlemnm  10451  resqrexlemcvg  10452  resqrexlemoverl  10454  resqrexlemglsq  10455  resqrexlemga  10456  clim2ser  10725  clim2ser2  10726  climrecvg1n  10737  climcvg1nlem  10738  serf0  10741  sumeq2  10748  fisumcvg  10766  fsum3cvg  10767  isummolem2a  10771  fisumss  10784  fsumcl2lem  10792  fsumadd  10800  fsummulc2  10842  fsumrelem  10865  isumshft  10884  cvgratnnlemseq  10920  cvgratnnlemrate  10924  effsumlt  10982  nn0seqcvgd  11301  ialgrlem1st  11302  elcncf2  11630  cncfco  11647  nnsf  11895  peano4nninf  11896  nninfalllem1  11899  nninfsellemdc  11902  nninfsellemeq  11906  nninfsellemqall  11907  nninfsellemeqinf  11908  nninfomnilem  11910
  Copyright terms: Public domain W3C validator