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

Theorem fveq2d 5213
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 5209 . 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 1285   ` cfv 4932
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940
This theorem is referenced by:  fveq12d  5215  csbfvg  5243  fvmptdf  5290  fvmptt  5294  fcof1  5454  oveq1  5550  oveq2  5551  caofinvl  5764  op1stg  5808  op2ndg  5809  ot1stg  5810  ot2ndg  5811  eloprabi  5853  1stconst  5873  algrflemg  5882  tfrlem1  5957  tfrlem3ag  5958  tfrlem3a  5959  tfrlem9  5968  tfr0dm  5971  tfrlemisucaccv  5974  tfrlemiubacc  5979  tfrlemiex  5980  tfrlemi1  5981  tfr1onlem3ag  5986  tfr1onlemsucaccv  5990  tfr1onlemubacc  5995  tfr1onlemex  5996  tfr1onlemaccex  5997  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllemubacc  6008  tfrcllemex  6009  tfrcllemaccex  6010  tfrcllemres  6011  tfrcldm  6012  rdgivallem  6030  rdgival  6031  rdgss  6032  rdgisuc1  6033  rdgon  6035  rdg0  6036  frec0g  6046  frecabcl  6048  freccllem  6051  frecfcllem  6053  frecsuclem  6055  frecsuc  6056  frecrdg  6057  oav2  6107  omv2  6109  xpdom2  6375  ac6sfi  6431  ltdfpr  6758  genpelvl  6764  genpelvu  6765  recexpr  6890  cauappcvgprlem1  6911  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemdisj  6926  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem1  6931  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemell  6937  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemnkeqj  6942  caucvgprprlemmu  6947  caucvgprprlemopl  6949  caucvgprprlemlol  6950  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem1  6961  caucvgprprlem2  6962  caucvgsr  7040  axcaucvglemval  7125  axcaucvglemres  7127  uzin  8732  cnref1o  8814  fzsuc2  9172  fseq1m1p1  9188  fzoss2  9258  elfzonlteqm1  9296  divfl0  9378  flqzadd  9380  fldiv4p1lem1div2  9387  ceilqval  9388  flqdiv  9403  modqval  9406  modqfrac  9419  modqmulnn  9424  modqid  9431  modqcyc  9441  modqdi  9474  frec2uzuzd  9484  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgtcl  9494  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgfunlem  9501  frecuzrdgsuctlem  9505  iseqovex  9529  iseqval  9530  iseqvalcbv  9531  iseqvalt  9532  iseqfclt  9536  iseqp1  9538  iseqp1t  9539  iseqm1  9543  iseqshft2  9548  monoord  9551  monoord2  9552  iseqhomo  9565  expival  9575  expnegap0  9581  facp1  9754  facnn2  9758  facwordi  9764  faclbnd6  9768  bcval  9773  bccmpl  9778  bcn0  9779  bcm1k  9784  bcp1n  9785  bcn2  9788  sizeinf  9802  sizeennn  9804  sizesng  9822  omgadd  9826  sizeprg  9832  shftval2  9852  shftval3  9853  shftval4  9854  shftval5  9855  imval  9875  imre  9876  reim  9877  crim  9883  reim0  9886  mulreap  9889  recj  9892  reneg  9893  readd  9894  resub  9895  remullem  9896  redivap  9899  imcj  9900  imneg  9901  imadd  9902  imsub  9903  imdivap  9906  cjsub  9917  cjexp  9918  cjreim2  9929  cjap  9931  cjdivap  9934  cnrecnv  9935  cvg1nlemcau  10008  cvg1nlemres  10009  absval  10025  rennim  10026  sqrtdiv  10066  sqrtmsq  10069  absneg  10074  abscj  10076  absval2  10081  absreim  10092  absmul  10093  absdivap  10094  absid  10095  absre  10101  absexp  10103  absexpzap  10104  absimle  10108  abssub  10125  abs3dif  10129  abs2dif  10130  abs2dif2  10131  recan  10133  cau3lem  10138  max0addsup  10243  clim  10258  clim2  10260  clim0  10262  clim0c  10263  climi0  10266  climconst  10267  climshftlemg  10279  climcn1  10285  climcn2  10286  addcn2  10287  subcn2  10288  mulcn2  10289  cjcn2  10292  recn2  10293  imcn2  10294  climcau  10322  climcvg1nlem  10324  climcvg1n  10325  serif0  10327  flodddiv4  10478  ialginv  10573  ialgcvg  10574  ialgcvga  10577  eucalgval  10580  eucalginv  10582  eucalglt  10583  eucialgcvga  10584  eucialg  10585  lcmgcd  10604  lcm1  10607  sqpweven  10697  2sqpwodd  10698  sqne2sq  10699  qdencn  10943
  Copyright terms: Public domain W3C validator