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

Theorem fveq2d 5274
Description: Equality deduction for function value. (Contributed by NM, 29-May-1999.)
Hypothesis
Ref Expression
fveq2d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
fveq2d  |-  ( ph  ->  ( F `  A
)  =  ( F `
 B ) )

Proof of Theorem fveq2d
StepHypRef Expression
1 fveq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 fveq2 5270 . 2  |-  ( A  =  B  ->  ( F `  A )  =  ( F `  B ) )
31, 2syl 14 1  |-  ( ph  ->  ( F `  A
)  =  ( F `
 B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1287   ` cfv 4983
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 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-iota 4948  df-fv 4991
This theorem is referenced by:  2fveq3  5275  fveq12d  5277  fveqeq2d  5278  csbfvg  5307  fvmptdf  5355  fvmptt  5359  fcof1  5525  oveq1  5622  oveq2  5623  caofinvl  5836  op1stg  5880  op2ndg  5881  ot1stg  5882  ot2ndg  5883  eloprabi  5925  1stconst  5945  algrflemg  5954  tfrlem1  6029  tfrlem3ag  6030  tfrlem3a  6031  tfrlem9  6040  tfr0dm  6043  tfrlemisucaccv  6046  tfrlemiubacc  6051  tfrlemiex  6052  tfrlemi1  6053  tfr1onlem3ag  6058  tfr1onlemsucaccv  6062  tfr1onlemubacc  6067  tfr1onlemex  6068  tfr1onlemaccex  6069  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllemubacc  6080  tfrcllemex  6081  tfrcllemaccex  6082  tfrcllemres  6083  tfrcldm  6084  rdgivallem  6102  rdgival  6103  rdgss  6104  rdgisuc1  6105  rdgon  6107  rdg0  6108  frec0g  6118  frecabcl  6120  freccllem  6123  frecfcllem  6125  frecsuclem  6127  frecsuc  6128  frecrdg  6129  oav2  6180  omv2  6182  xpdom2  6501  xpmapenlem  6519  xpmapen  6520  ac6sfi  6568  1stinl  6712  2ndinl  6713  1stinr  6714  2ndinr  6715  updjudhcoinlf  6718  updjudhcoinrg  6719  enomnilem  6741  exmidfodomrlemeldju  6772  exmidfodomrlemreseldju  6773  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  ltdfpr  7012  genpelvl  7018  genpelvu  7019  recexpr  7144  cauappcvgprlem1  7165  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemm  7174  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem1  7185  caucvgprlem2  7186  caucvgpr  7188  caucvgprprlemell  7191  caucvgprprlemelu  7192  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemnkeqj  7196  caucvgprprlemmu  7201  caucvgprprlemopl  7203  caucvgprprlemlol  7204  caucvgprprlemopu  7205  caucvgprprlemloc  7209  caucvgprprlemclphr  7211  caucvgprprlemexbt  7212  caucvgprprlem1  7215  caucvgprprlem2  7216  caucvgsr  7294  axcaucvglemval  7379  axcaucvglemres  7381  uzin  8986  cnref1o  9068  fzsuc2  9426  fseq1m1p1  9442  fzoss2  9514  elfzonlteqm1  9552  divfl0  9634  flqzadd  9636  fldiv4p1lem1div2  9643  ceilqval  9644  flqdiv  9659  modqval  9662  modqfrac  9675  modqmulnn  9680  modqid  9687  modqcyc  9697  modqdi  9730  frec2uzuzd  9740  frec2uzrdg  9747  frecuzrdgrcl  9748  frecuzrdgtcl  9750  frecuzrdgsuc  9752  frecuzrdgrclt  9753  frecuzrdgg  9754  frecuzrdgfunlem  9757  frecuzrdgsuctlem  9761  iseqovex  9801  iseqval  9802  iseqvalcbv  9803  iseqvalt  9804  iseqfclt  9809  iseqp1  9812  iseqp1t  9813  iseqm1  9819  iseqshft2  9824  monoord  9829  monoord2  9830  iseqf1olemqval  9840  iseqf1olemab  9842  iseqf1olemqk  9847  iseqf1olemjpcl  9848  iseqf1olemqpcl  9849  iseqf1olemfvp  9850  iseqf1olemqsumkj  9851  iseqf1olemqsumk  9852  iseqf1olemqsum  9853  iseqf1olemp  9855  iseqf1oleml  9856  iseqf1o  9857  iseqhomo  9864  expival  9877  expnegap0  9883  facp1  10056  facnn2  10060  facwordi  10066  faclbnd6  10070  bcval  10075  bccmpl  10080  bcn0  10081  bcm1k  10086  bcp1n  10087  bcn2  10090  hashinfom  10104  hashennn  10106  hashsng  10124  omgadd  10128  hashprg  10134  fihashssdif  10144  hashdifpr  10146  hashfzo  10148  hashfzp1  10150  hashxp  10152  zfz1isolemiso  10162  zfz1iso  10164  shftval2  10178  shftval3  10179  shftval4  10180  shftval5  10181  imval  10201  imre  10202  reim  10203  crim  10209  reim0  10212  mulreap  10215  recj  10218  reneg  10219  readd  10220  resub  10221  remullem  10222  redivap  10225  imcj  10226  imneg  10227  imadd  10228  imsub  10229  imdivap  10232  cjsub  10243  cjexp  10244  cjreim2  10255  cjap  10257  cjdivap  10260  cnrecnv  10261  cvg1nlemcau  10334  cvg1nlemres  10335  absval  10351  rennim  10352  sqrtdiv  10392  sqrtmsq  10395  absneg  10400  abscj  10402  absval2  10407  absreim  10418  absmul  10419  absdivap  10420  absid  10421  absre  10427  absexp  10429  absexpzap  10430  absimle  10434  abssub  10451  abs3dif  10455  abs2dif  10456  abs2dif2  10457  recan  10459  cau3lem  10464  max0addsup  10569  clim  10585  clim2  10587  clim0  10589  clim0c  10590  climi0  10593  climconst  10594  climshftlemg  10606  climcn1  10613  climcn2  10614  addcn2  10615  subcn2  10616  mulcn2  10617  cjcn2  10620  recn2  10621  imcn2  10622  climcau  10650  climcvg1nlem  10652  climcvg1n  10653  serif0  10655  isummolem3  10683  isummolem2a  10684  isummo  10686  fsumf1o  10692  sumsnf  10710  fsumm1  10716  flodddiv4  10859  ialginv  10954  ialgcvg  10955  ialgcvga  10958  eucalgval  10961  eucalginv  10963  eucalglt  10964  eucialgcvga  10965  eucialg  10966  lcmgcd  10985  lcm1  10988  sqpweven  11078  2sqpwodd  11079  sqne2sq  11080  qnumval  11088  qdenval  11089  qden1elz  11108  nn0sqrtelqelz  11109  phival  11114  dfphi2  11121  phiprmpw  11123  phiprm  11124  hashgcdeq  11129  nnsf  11383  peano4nninf  11384  peano3nninf  11385  nninfalllemn  11386  nninfalllem1  11387  nninfall  11388  nninfsellemdc  11390  nninfsellemeq  11394  nninfsellemqall  11395  nninfsellemeqinf  11396  nninfsel  11397  nninfomni  11399  exmidsbthr  11401  qdencn  11403
  Copyright terms: Public domain W3C validator