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

Theorem fveq2d 5272
Description: Equality deduction for function value. (Contributed by NM, 29-May-1999.)
Hypothesis
Ref Expression
fveq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
fveq2d (𝜑 → (𝐹𝐴) = (𝐹𝐵))

Proof of Theorem fveq2d
StepHypRef Expression
1 fveq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 fveq2 5268 . 2 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  cfv 4981
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 3637  df-br 3821  df-iota 4946  df-fv 4989
This theorem is referenced by:  2fveq3  5273  fveq12d  5275  fveqeq2d  5276  csbfvg  5305  fvmptdf  5353  fvmptt  5357  fcof1  5523  oveq1  5620  oveq2  5621  caofinvl  5834  op1stg  5878  op2ndg  5879  ot1stg  5880  ot2ndg  5881  eloprabi  5923  1stconst  5943  algrflemg  5952  tfrlem1  6027  tfrlem3ag  6028  tfrlem3a  6029  tfrlem9  6038  tfr0dm  6041  tfrlemisucaccv  6044  tfrlemiubacc  6049  tfrlemiex  6050  tfrlemi1  6051  tfr1onlem3ag  6056  tfr1onlemsucaccv  6060  tfr1onlemubacc  6065  tfr1onlemex  6066  tfr1onlemaccex  6067  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllemubacc  6078  tfrcllemex  6079  tfrcllemaccex  6080  tfrcllemres  6081  tfrcldm  6082  rdgivallem  6100  rdgival  6101  rdgss  6102  rdgisuc1  6103  rdgon  6105  rdg0  6106  frec0g  6116  frecabcl  6118  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecsuc  6126  frecrdg  6127  oav2  6178  omv2  6180  xpdom2  6499  xpmapenlem  6517  xpmapen  6518  ac6sfi  6566  1stinl  6709  2ndinl  6710  1stinr  6711  2ndinr  6712  updjudhcoinlf  6715  updjudhcoinrg  6716  enomnilem  6738  exmidfodomrlemeldju  6769  exmidfodomrlemreseldju  6770  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  ltdfpr  7009  genpelvl  7015  genpelvu  7016  recexpr  7141  cauappcvgprlem1  7162  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgprlem2  7183  caucvgpr  7185  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnkeqj  7193  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemclphr  7208  caucvgprprlemexbt  7209  caucvgprprlem1  7212  caucvgprprlem2  7213  caucvgsr  7291  axcaucvglemval  7376  axcaucvglemres  7378  uzin  8983  cnref1o  9065  fzsuc2  9423  fseq1m1p1  9439  fzoss2  9511  elfzonlteqm1  9549  divfl0  9631  flqzadd  9633  fldiv4p1lem1div2  9640  ceilqval  9641  flqdiv  9656  modqval  9659  modqfrac  9672  modqmulnn  9677  modqid  9684  modqcyc  9694  modqdi  9727  frec2uzuzd  9737  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgtcl  9747  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgfunlem  9754  frecuzrdgsuctlem  9758  iseqovex  9787  iseqval  9788  iseqvalcbv  9789  iseqvalt  9790  iseqfclt  9794  iseqp1  9796  iseqp1t  9797  iseqm1  9801  iseqshft2  9806  monoord  9809  monoord2  9810  iseqf1olemqval  9820  iseqf1olemab  9822  iseqf1olemqk  9827  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemfvp  9830  iseqf1olemqsumkj  9831  iseqf1olemqsumk  9832  iseqf1olemqsum  9833  iseqf1olemp  9835  iseqf1oleml  9836  iseqf1o  9837  iseqhomo  9844  expival  9855  expnegap0  9861  facp1  10034  facnn2  10038  facwordi  10044  faclbnd6  10048  bcval  10053  bccmpl  10058  bcn0  10059  bcm1k  10064  bcp1n  10065  bcn2  10068  hashinfom  10082  hashennn  10084  hashsng  10102  omgadd  10106  hashprg  10112  fihashssdif  10122  hashdifpr  10124  hashfzo  10126  hashfzp1  10128  hashxp  10130  zfz1isolemiso  10140  zfz1iso  10142  shftval2  10156  shftval3  10157  shftval4  10158  shftval5  10159  imval  10179  imre  10180  reim  10181  crim  10187  reim0  10190  mulreap  10193  recj  10196  reneg  10197  readd  10198  resub  10199  remullem  10200  redivap  10203  imcj  10204  imneg  10205  imadd  10206  imsub  10207  imdivap  10210  cjsub  10221  cjexp  10222  cjreim2  10233  cjap  10235  cjdivap  10238  cnrecnv  10239  cvg1nlemcau  10312  cvg1nlemres  10313  absval  10329  rennim  10330  sqrtdiv  10370  sqrtmsq  10373  absneg  10378  abscj  10380  absval2  10385  absreim  10396  absmul  10397  absdivap  10398  absid  10399  absre  10405  absexp  10407  absexpzap  10408  absimle  10412  abssub  10429  abs3dif  10433  abs2dif  10434  abs2dif2  10435  recan  10437  cau3lem  10442  max0addsup  10547  clim  10562  clim2  10564  clim0  10566  clim0c  10567  climi0  10570  climconst  10571  climshftlemg  10583  climcn1  10589  climcn2  10590  addcn2  10591  subcn2  10592  mulcn2  10593  cjcn2  10596  recn2  10597  imcn2  10598  climcau  10626  climcvg1nlem  10628  climcvg1n  10629  serif0  10631  isummolem3  10659  isummolem2a  10660  isummo  10662  fsumf1o  10668  flodddiv4  10809  ialginv  10904  ialgcvg  10905  ialgcvga  10908  eucalgval  10911  eucalginv  10913  eucalglt  10914  eucialgcvga  10915  eucialg  10916  lcmgcd  10935  lcm1  10938  sqpweven  11028  2sqpwodd  11029  sqne2sq  11030  qnumval  11038  qdenval  11039  qden1elz  11058  nn0sqrtelqelz  11059  phival  11064  dfphi2  11071  phiprmpw  11073  phiprm  11074  hashgcdeq  11079  nnsf  11333  peano4nninf  11334  peano3nninf  11335  nninfalllemn  11336  nninfalllem1  11337  nninfall  11338  nninfsellemdc  11340  nninfsellemeq  11344  nninfsellemqall  11345  nninfsellemeqinf  11346  nninfsel  11347  nninfomni  11349  exmidsbthr  11351  qdencn  11353
  Copyright terms: Public domain W3C validator