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

Theorem fveq2d 5207
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 5203 . 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 1257   ` cfv 4927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-3an 896  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-rex 2327  df-v 2574  df-un 2947  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-br 3790  df-iota 4892  df-fv 4935
This theorem is referenced by:  fveq12d  5209  csbfvg  5236  fvmptdf  5283  fvmptt  5287  fcof1  5448  oveq1  5544  oveq2  5545  caofinvl  5758  op1stg  5802  op2ndg  5803  ot1stg  5804  ot2ndg  5805  eloprabi  5847  1stconst  5867  algrflemg  5876  tfrlem1  5951  tfrlem3ag  5952  tfrlem3a  5953  tfrlem9  5963  tfr0  5965  tfrlemisucaccv  5967  tfrlemiubacc  5972  tfrlemiex  5973  tfrlemi1  5974  rdgivallem  5996  rdgival  5997  rdgss  5998  rdgisuc1  5999  rdg0  6002  frec0g  6011  frecsuclem3  6018  frecsuc  6019  frecrdg  6020  oav2  6071  omv2  6073  xpdom2  6333  ac6sfi  6380  ltdfpr  6632  genpelvl  6638  genpelvu  6639  recexpr  6764  cauappcvgprlem1  6785  caucvgprlemnkj  6792  caucvgprlemnbj  6793  caucvgprlemm  6794  caucvgprlemdisj  6800  caucvgprlemloc  6801  caucvgprlemcl  6802  caucvgprlemladdfu  6803  caucvgprlemladdrl  6804  caucvgprlem1  6805  caucvgprlem2  6806  caucvgpr  6808  caucvgprprlemell  6811  caucvgprprlemelu  6812  caucvgprprlemcbv  6813  caucvgprprlemval  6814  caucvgprprlemnkeqj  6816  caucvgprprlemmu  6821  caucvgprprlemopl  6823  caucvgprprlemlol  6824  caucvgprprlemopu  6825  caucvgprprlemloc  6829  caucvgprprlemclphr  6831  caucvgprprlemexbt  6832  caucvgprprlem1  6835  caucvgprprlem2  6836  caucvgsr  6914  axcaucvglemval  6999  axcaucvglemres  7001  uzin  8571  cnref1o  8650  fzsuc2  9013  fseq1m1p1  9029  fzoss2  9100  elfzonlteqm1  9138  divfl0  9211  flqzadd  9213  fldiv4p1lem1div2  9220  ceilqval  9221  flqdiv  9236  modqval  9239  modqfrac  9252  modqmulnn  9257  modqid  9264  modqcyc  9274  modqdi  9307  frec2uzzd  9315  frec2uzuzd  9317  frec2uzrdg  9324  frecuzrdgfn  9327  frecuzrdgsuc  9330  iseqovex  9348  iseqval  9349  iseqp1  9354  iseqm1  9356  iseqshft2  9361  monoord  9364  monoord2  9365  iseqhomo  9377  expival  9387  expnegap0  9393  facp1  9562  facnn2  9566  facwordi  9572  faclbnd6  9576  bcval  9581  bccmpl  9586  bcn0  9587  bcm1k  9592  bcp1n  9593  bcn2  9596  shftval2  9619  shftval3  9620  shftval4  9621  shftval5  9622  imval  9642  imre  9643  reim  9644  crim  9650  reim0  9653  mulreap  9656  recj  9659  reneg  9660  readd  9661  resub  9662  remullem  9663  redivap  9666  imcj  9667  imneg  9668  imadd  9669  imsub  9670  imdivap  9673  cjsub  9684  cjexp  9685  cjreim2  9696  cjap  9698  cjdivap  9701  cnrecnv  9702  cvg1nlemcau  9775  cvg1nlemres  9776  absval  9791  rennim  9792  sqrtdiv  9832  sqrtmsq  9835  absneg  9840  abscj  9842  absval2  9847  absreim  9858  absmul  9859  absdivap  9860  absid  9861  absre  9867  absexp  9869  absexpzap  9870  absimle  9874  abssub  9891  abs3dif  9895  abs2dif  9896  abs2dif2  9897  recan  9899  cau3lem  9904  clim  9996  clim2  9998  clim0  10000  clim0c  10001  climi0  10004  climconst  10005  climshftlemg  10017  climcn1  10023  climcn2  10024  addcn2  10025  subcn2  10026  mulcn2  10027  cjcn2  10030  recn2  10031  imcn2  10032  climcau  10060  climcvg1nlem  10062  climcvg1n  10063  serif0  10065  ialginv  10212  ialgcvg  10213  ialgcvga  10216  qdencn  10454
  Copyright terms: Public domain W3C validator