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

Theorem ffvelrnda 5523
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 5521 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2sylan 281 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1465   -->wf 5089   ` cfv 5093
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-pow 4068  ax-pr 4101
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-sbc 2883  df-un 3045  df-in 3047  df-ss 3054  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-opab 3960  df-id 4185  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-fv 5101
This theorem is referenced by:  ffvelrnd  5524  f1ocnvdm  5650  foeqcnvco  5659  f1oiso2  5696  offeq  5963  suppssof1  5967  ofco  5968  caofref  5971  caofinvl  5972  caofcom  5973  caofrss  5974  caoftrn  5975  smofvon2dm  6161  smofvon  6164  mapxpen  6710  xpmapenlem  6711  en2eqpr  6769  supisoex  6864  ordiso2  6888  omp1eomlem  6947  ctssdccl  6964  ctssdc  6966  enumctlemm  6967  enomnilem  6978  fodjuomnilemdc  6984  ismkvnex  6997  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemladdrl  7454  caucvgprprlemopu  7475  caucvgprprlemexbt  7482  caucvgprprlemexb  7483  caucvgsrlemcl  7565  caucvgsrlemfv  7567  caucvgsrlemcau  7569  caucvgsrlembound  7570  caucvgsrlemoffval  7572  caucvgsrlemofff  7573  caucvgsrlemoffgt1  7575  caucvgsrlemoffres  7576  caucvgsr  7578  axcaucvglemcl  7671  frecuzrdgfunlem  10147  monoord2  10205  seq3f1o  10232  seq3homo  10238  seqfeq3  10240  zfz1isolemiso  10537  seq3coll  10540  resqrexlemfp1  10736  resqrexlemover  10737  resqrexlemdec  10738  resqrexlemlo  10740  resqrexlemcalc1  10741  resqrexlemcalc2  10742  resqrexlemcalc3  10743  resqrexlemgt0  10747  resqrexlemsqa  10751  clim2ser  11061  clim2ser2  11062  isermulc2  11064  iserle  11066  climserle  11069  climrecvg1n  11072  climcvg1nlem  11073  summodclem3  11104  summodclem2a  11105  fsumgcl  11110  fsum3  11111  fsumf1o  11114  isumss  11115  fisumss  11116  fsumcl2lem  11122  fsumadd  11130  isumclim3  11147  isummulc2  11150  isumrecl  11153  isumadd  11155  fsummulc2  11172  iserabs  11199  cvgcmpub  11200  isumshft  11214  isumsplit  11215  mertensabs  11261  efcj  11293  nn0seqcvgd  11634  algrp1  11639  alginv  11640  algcvg  11641  algcvga  11644  algfx  11645  eucalgcvga  11651  cnptoprest2  12320  lmss  12326  txcnmpt  12353  txlm  12359  lmcn2  12360  psmetxrge0  12412  metcnp  12592  climcncf  12651  negfcncf  12669  ivthdec  12702  dvcnp2cntop  12743  dvaddxxbr  12745  dvimulf  12750  dvcj  12753  dvfre  12754  nninfall  13100  nninffeq  13112  refeq  13119  trilpolemclim  13125  trilpolemcl  13126  trilpolemisumle  13127  trilpolemeq1  13129
  Copyright terms: Public domain W3C validator