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

Theorem ffvelrnda 5521
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 5519 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2sylan 279 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1463   -->wf 5087   ` cfv 5091
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-sbc 2881  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-id 4183  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-fv 5099
This theorem is referenced by:  ffvelrnd  5522  f1ocnvdm  5648  foeqcnvco  5657  f1oiso2  5694  offeq  5961  suppssof1  5965  ofco  5966  caofref  5969  caofinvl  5970  caofcom  5971  caofrss  5972  caoftrn  5973  smofvon2dm  6159  smofvon  6162  mapxpen  6708  xpmapenlem  6709  en2eqpr  6767  supisoex  6862  ordiso2  6886  omp1eomlem  6945  ctssdccl  6962  ctssdc  6964  enumctlemm  6965  enomnilem  6976  fodjuomnilemdc  6982  ismkvnex  6995  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  caucvgprlemladdrl  7450  caucvgprprlemopu  7471  caucvgprprlemexbt  7478  caucvgprprlemexb  7479  caucvgsrlemcl  7561  caucvgsrlemfv  7563  caucvgsrlemcau  7565  caucvgsrlembound  7566  caucvgsrlemoffval  7568  caucvgsrlemofff  7569  caucvgsrlemoffgt1  7571  caucvgsrlemoffres  7572  caucvgsr  7574  axcaucvglemcl  7667  frecuzrdgfunlem  10132  monoord2  10190  seq3f1o  10217  seq3homo  10223  seqfeq3  10225  zfz1isolemiso  10522  seq3coll  10525  resqrexlemfp1  10721  resqrexlemover  10722  resqrexlemdec  10723  resqrexlemlo  10725  resqrexlemcalc1  10726  resqrexlemcalc2  10727  resqrexlemcalc3  10728  resqrexlemgt0  10732  resqrexlemsqa  10736  clim2ser  11046  clim2ser2  11047  isermulc2  11049  iserle  11051  climserle  11054  climrecvg1n  11057  climcvg1nlem  11058  summodclem3  11089  summodclem2a  11090  fsumgcl  11095  fsum3  11096  fsumf1o  11099  isumss  11100  fisumss  11101  fsumcl2lem  11107  fsumadd  11115  isumclim3  11132  isummulc2  11135  isumrecl  11138  isumadd  11140  fsummulc2  11157  iserabs  11184  cvgcmpub  11185  isumshft  11199  isumsplit  11200  mertensabs  11246  efcj  11278  nn0seqcvgd  11618  algrp1  11623  alginv  11624  algcvg  11625  algcvga  11628  algfx  11629  eucalgcvga  11635  cnptoprest2  12304  lmss  12310  txcnmpt  12337  txlm  12343  lmcn2  12344  psmetxrge0  12396  metcnp  12576  climcncf  12635  negfcncf  12653  dvcnp2cntop  12706  dvaddxxbr  12708  dvimulf  12713  dvcj  12716  dvfre  12717  nninfall  13006  nninffeq  13018  refeq  13025  trilpolemclim  13031  trilpolemcl  13032  trilpolemisumle  13033  trilpolemeq1  13035
  Copyright terms: Public domain W3C validator