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

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

Proof of Theorem ffvelrnda
StepHypRef Expression
1 ffvelrnd.1 . 2  |-  ( ph  ->  F : A --> B )
2 ffvelrn 5432 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2sylan 277 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    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:  ffvelrnd  5435  f1ocnvdm  5560  foeqcnvco  5569  f1oiso2  5606  suppssof1  5872  ofco  5873  caofref  5876  caofinvl  5877  caofcom  5878  caofrss  5879  caoftrn  5880  smofvon2dm  6061  smofvon  6064  mapxpen  6562  xpmapenlem  6563  en2eqpr  6621  supisoex  6702  ordiso2  6726  enomnilem  6792  fodjuomnilemdc  6797  cauappcvgprlemladdru  7213  cauappcvgprlemladdrl  7214  caucvgprlemladdrl  7235  caucvgprprlemopu  7256  caucvgprprlemexbt  7263  caucvgprprlemexb  7264  caucvgsrlemcl  7332  caucvgsrlemfv  7334  caucvgsrlemcau  7336  caucvgsrlembound  7337  caucvgsrlemoffval  7339  caucvgsrlemofff  7340  caucvgsrlemoffgt1  7342  caucvgsrlemoffres  7343  caucvgsr  7345  axcaucvglemcl  7428  frecuzrdgfunlem  9822  monoord2  9901  seq3f1o  9929  seq3homo  9940  zfz1isolemiso  10240  iseqcoll  10243  resqrexlemfp1  10438  resqrexlemover  10439  resqrexlemdec  10440  resqrexlemlo  10442  resqrexlemcalc1  10443  resqrexlemcalc2  10444  resqrexlemcalc3  10445  resqrexlemgt0  10449  resqrexlemsqa  10453  clim2ser  10721  clim2ser2  10722  iisermulc2  10724  iserle  10727  climserle  10730  climrecvg1n  10733  climcvg1nlem  10734  isummolem3  10766  isummolem2a  10767  fsumgcl  10773  fisum  10774  fsumf1o  10778  isumss  10779  fisumss  10780  fsumcl2lem  10788  fsumadd  10796  isumclim3  10813  isummulc2  10816  isumrecl  10819  isumadd  10821  fsummulc2  10838  iserabs  10865  cvgcmpub  10866  isumshft  10880  isumsplit  10881  mertensabs  10927  efcj  10959  nn0seqcvgd  11297  ialginv  11303  ialgcvg  11304  ialgcvga  11307  ialgfx  11308  eucialgcvga  11314  climcncf  11595  nninfall  11855
  Copyright terms: Public domain W3C validator