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

Theorem fveq2d 5182
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 5178 . 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 1243   ` cfv 4902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910
This theorem is referenced by:  fveq12d  5184  csbfvg  5211  fvmptdf  5258  fvmptt  5262  fcof1  5423  oveq1  5519  oveq2  5520  caofinvl  5733  op1stg  5777  op2ndg  5778  ot1stg  5779  ot2ndg  5780  eloprabi  5822  1stconst  5842  algrflemg  5851  tfrlem1  5923  tfrlem3ag  5924  tfrlem3a  5925  tfrlem9  5935  tfr0  5937  tfrlemisucaccv  5939  tfrlemiubacc  5944  tfrlemiex  5945  tfrlemi1  5946  rdgivallem  5968  rdgival  5969  rdgss  5970  rdgisuc1  5971  rdg0  5974  frec0g  5983  frecsuclem3  5990  frecsuc  5991  frecrdg  5992  oav2  6043  omv2  6045  xpdom2  6305  ac6sfi  6352  ltdfpr  6604  genpelvl  6610  genpelvu  6611  recexpr  6736  cauappcvgprlem1  6757  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprlem2  6778  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkeqj  6788  caucvgprprlemmu  6793  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlem1  6807  caucvgprprlem2  6808  caucvgsr  6886  axcaucvglemval  6971  axcaucvglemres  6973  uzin  8505  cnref1o  8582  fzsuc2  8941  fseq1m1p1  8957  fzoss2  9028  elfzonlteqm1  9066  divfl0  9138  flqzadd  9140  fldiv4p1lem1div2  9147  ceilqval  9148  flqdiv  9163  modqval  9166  modqfrac  9179  modqmulnn  9184  frec2uzzd  9186  frec2uzuzd  9188  frec2uzrdg  9195  frecuzrdgfn  9198  frecuzrdgsuc  9201  iseqovex  9219  iseqval  9220  iseqp1  9225  iseqm1  9227  iseqshft2  9232  monoord  9235  monoord2  9236  iseqhomo  9248  expival  9257  expnegap0  9263  shftval2  9427  shftval3  9428  shftval4  9429  shftval5  9430  imval  9450  imre  9451  reim  9452  crim  9458  reim0  9461  mulreap  9464  recj  9467  reneg  9468  readd  9469  resub  9470  remullem  9471  redivap  9474  imcj  9475  imneg  9476  imadd  9477  imsub  9478  imdivap  9481  cjsub  9492  cjexp  9493  cjreim2  9504  cjap  9506  cjdivap  9509  cnrecnv  9510  cvg1nlemcau  9583  cvg1nlemres  9584  absval  9599  rennim  9600  sqrtdiv  9640  sqrtmsq  9643  absneg  9648  abscj  9650  absval2  9655  absreim  9666  absmul  9667  absdivap  9668  absid  9669  absre  9673  absexp  9675  absexpzap  9676  absimle  9680  abssub  9697  abs3dif  9701  abs2dif  9702  abs2dif2  9703  recan  9705  cau3lem  9710  clim  9802  clim2  9804  clim0  9806  clim0c  9807  climi0  9810  climconst  9811  climshftlemg  9823  climcn1  9829  climcn2  9830  addcn2  9831  subcn2  9832  mulcn2  9833  cjcn2  9836  recn2  9837  imcn2  9838  climcau  9866  climcvg1nlem  9868  climcvg1n  9869  serif0  9871  ialginv  9886  ialgcvg  9887  ialgcvga  9890  qdencn  10123
  Copyright terms: Public domain W3C validator