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

Theorem fveq2d 5425
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 5421 . 2 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐹𝐴) = (𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  cfv 5123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131
This theorem is referenced by:  2fveq3  5426  fveq12d  5428  fveqeq2d  5429  csbfvg  5459  fvmptdf  5508  fvmptt  5512  fcof1  5684  oveq1  5781  oveq2  5782  fvoveq1d  5796  caofinvl  6004  op1stg  6048  op2ndg  6049  ot1stg  6050  ot2ndg  6051  eloprabi  6094  1stconst  6118  algrflemg  6127  tfrlem1  6205  tfrlem3ag  6206  tfrlem3a  6207  tfrlem9  6216  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfrlemiex  6228  tfrlemi1  6229  tfr1onlem3ag  6234  tfr1onlemsucaccv  6238  tfr1onlemubacc  6243  tfr1onlemex  6244  tfr1onlemaccex  6245  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemubacc  6256  tfrcllemex  6257  tfrcllemaccex  6258  tfrcllemres  6259  tfrcldm  6260  rdgivallem  6278  rdgival  6279  rdgss  6280  rdgisuc1  6281  rdgon  6283  rdg0  6284  frec0g  6294  frecabcl  6296  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  frecrdg  6305  oav2  6359  omv2  6361  xpdom2  6725  xpmapenlem  6743  xpmapen  6744  ac6sfi  6792  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  updjudhcoinlf  6965  updjudhcoinrg  6966  caseinl  6976  caseinr  6977  omp1eomlem  6979  omp1eom  6980  difinfsn  6985  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  enomnilem  7010  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  cc2  7082  cc3  7083  ltdfpr  7321  genpelvl  7327  genpelvu  7328  recexpr  7453  cauappcvgprlem1  7474  caucvgprlemnkj  7481  caucvgprlemnbj  7482  caucvgprlemm  7483  caucvgprlemdisj  7489  caucvgprlemloc  7490  caucvgprlemcl  7491  caucvgprlemladdfu  7492  caucvgprlemladdrl  7493  caucvgprlem1  7494  caucvgprlem2  7495  caucvgpr  7497  caucvgprprlemell  7500  caucvgprprlemelu  7501  caucvgprprlemcbv  7502  caucvgprprlemval  7503  caucvgprprlemnkeqj  7505  caucvgprprlemmu  7510  caucvgprprlemopl  7512  caucvgprprlemlol  7513  caucvgprprlemopu  7514  caucvgprprlemloc  7518  caucvgprprlemclphr  7520  caucvgprprlemexbt  7521  caucvgprprlem1  7524  caucvgprprlem2  7525  caucvgsr  7617  axcaucvglemval  7712  axcaucvglemres  7714  fv0p1e1  8842  uzin  9365  cnref1o  9447  fzsuc2  9866  fseq1m1p1  9882  fzoss2  9956  elfzonlteqm1  9994  divfl0  10076  flqzadd  10078  fldiv4p1lem1div2  10085  ceilqval  10086  flqdiv  10101  modqval  10104  modqfrac  10117  modqmulnn  10122  modqid  10129  modqcyc  10139  modqdi  10172  frec2uzuzd  10182  frec2uzrdg  10189  frecuzrdgrcl  10190  frecuzrdgtcl  10192  frecuzrdgsuc  10194  frecuzrdgrclt  10195  frecuzrdgg  10196  frecuzrdgfunlem  10199  frecuzrdgsuctlem  10203  iseqovex  10236  iseqvalcbv  10237  seq3val  10238  seqvalcd  10239  seq3m1  10248  seq3shft2  10253  monoord  10256  monoord2  10257  iseqf1olemqval  10267  iseqf1olemab  10269  iseqf1olemqk  10274  iseqf1olemjpcl  10275  iseqf1olemqpcl  10276  iseqf1olemfvp  10277  seq3f1olemqsumkj  10278  seq3f1olemqsumk  10279  seq3f1olemqsum  10280  seq3f1olemp  10282  seq3f1oleml  10283  seq3homo  10290  exp3val  10302  expnegap0  10308  facnn2  10487  facwordi  10493  faclbnd6  10497  bcval  10502  bccmpl  10507  bcn0  10508  bcm1k  10513  bcp1n  10514  bcn2  10517  hashinfom  10531  hashennn  10533  hashsng  10551  omgadd  10555  hashprg  10561  fihashssdif  10571  hashdifpr  10573  hashfzo  10575  hashfzp1  10577  hashxp  10579  zfz1isolemiso  10589  zfz1iso  10591  shftval2  10605  shftval3  10606  shftval4  10607  shftval5  10608  seq3shft  10617  imval  10629  imre  10630  reim  10631  crim  10637  reim0  10640  mulreap  10643  recj  10646  reneg  10647  readd  10648  resub  10649  remullem  10650  redivap  10653  imcj  10654  imneg  10655  imadd  10656  imsub  10657  imdivap  10660  cjsub  10671  cjexp  10672  cjreim2  10683  cjap  10685  cjdivap  10688  cnrecnv  10689  cvg1nlemcau  10763  cvg1nlemres  10764  absval  10780  rennim  10781  sqrtdiv  10821  sqrtmsq  10824  absneg  10829  abscj  10831  absval2  10836  absreim  10847  absmul  10848  absdivap  10849  absid  10850  absre  10856  absexp  10858  absexpzap  10859  absimle  10863  abssub  10880  abs3dif  10884  abs2dif  10885  abs2dif2  10886  recan  10888  cau3lem  10893  max0addsup  10998  minabs  11014  bdtrilem  11017  clim  11057  clim2  11059  clim0  11061  clim0c  11062  climi0  11065  climconst  11066  climshftlemg  11078  climcn1  11084  climcn2  11085  addcn2  11086  subcn2  11087  mulcn2  11088  reccn2ap  11089  cjcn2  11092  recn2  11093  imcn2  11094  iser3shft  11122  climcau  11123  climcvg1nlem  11125  climcvg1n  11126  serf0  11128  summodclem3  11156  summodclem2a  11157  summodc  11159  fsumf1o  11166  sumsnf  11185  fsumm1  11192  fsumcnv  11213  fsumabs  11241  fsumrelem  11247  iserabs  11251  hash2iun1dif1  11256  isumshft  11266  isumsplit  11267  expcnvap0  11278  expcnv  11280  cvgratnnlemseq  11302  cvgratnnlemrate  11306  cvgratz  11308  mertenslemub  11310  mertenslemi1  11311  mertenslem2  11312  mertensabs  11313  prodmodclem3  11351  efcllemp  11371  efcj  11386  efaddlem  11387  efcan  11389  efsub  11394  efexp  11395  efzval  11396  efgt0  11397  eftlub  11403  efltim  11411  sinval  11416  cosval  11417  tanval3ap  11428  resinval  11429  recosval  11430  resin4p  11432  recos4p  11433  sinneg  11440  cosneg  11441  efmival  11447  efeul  11448  sinadd  11450  cosadd  11451  sinsub  11454  cossub  11455  addsin  11456  subsin  11457  addcos  11460  subcos  11461  sincossq  11462  sin2t  11463  cos2t  11464  sin01bnd  11471  cos01bnd  11472  sin02gt0  11477  cos12dec  11481  absefi  11482  absef  11483  absefib  11484  efieq1re  11485  demoivre  11486  demoivreALT  11487  flodddiv4  11638  alginv  11735  algcvg  11736  eucalgval  11742  eucalginv  11744  eucalglt  11745  eucalgcvga  11746  eucalg  11747  lcmgcd  11766  lcm1  11769  sqpweven  11860  2sqpwodd  11861  sqne2sq  11862  qnumval  11870  qdenval  11871  qden1elz  11890  nn0sqrtelqelz  11891  phival  11896  dfphi2  11903  phiprmpw  11905  phiprm  11906  hashgcdeq  11911  ennnfonelemg  11923  ennnfonelemp1  11926  ennnfonelemkh  11932  ennnfonelemhf1o  11933  ennnfonelemnn0  11942  ctinfomlemom  11947  ctiunctlemu1st  11954  ctiunctlemu2nd  11955  ctiunctlemudc  11957  ctiunctlemfo  11959  isstruct2im  11979  isstruct2r  11980  strslfv3  12014  setsslid  12019  ressid2  12028  ressval2  12029  istps  12209  tpspropd  12213  eltpsg  12217  txvalex  12433  txval  12434  txbasval  12446  upxp  12451  uptx  12453  txrest  12455  cnmpt11  12462  cnmpt21  12470  hmeontr  12492  txhmeo  12498  psmetxrge0  12511  xmetunirn  12537  mopnval  12621  mopntopon  12622  isxms  12630  isxms2  12631  isms  12632  msrtri  12655  xmspropd  12656  mspropd  12657  setsmsbasg  12658  setsmsdsg  12659  setsmstsetg  12660  comet  12678  metcnpi  12694  metcnpi2  12695  cnbl0  12713  cnblcld  12714  resubmet  12727  elcncf  12739  cncfi  12744  rescncf  12747  mulc1cncf  12755  cncfco  12757  cncfmptid  12762  addccncf  12765  cdivcncfap  12766  negcncf  12767  mulcncflem  12769  ivthinclemlopn  12793  ivthinclemuopn  12795  limccl  12807  ellimc3apf  12808  limcimolemlt  12812  cnplimclemle  12816  limccnpcntop  12823  reldvg  12827  dvfvalap  12829  dveflem  12865  dvef  12866  sin0pilem1  12872  ef2kpi  12897  sinperlem  12899  sin2kpi  12902  cos2kpi  12903  sin2pim  12904  cos2pim  12905  ptolemy  12915  sincosq2sgn  12918  sincosq3sgn  12919  sincosq4sgn  12920  sinq12gt0  12921  tangtx  12929  sincosq1eq  12930  abssinper  12937  sinkpi  12938  coskpi  12939  cosq34lt1  12941  nnsf  13213  peano4nninf  13214  peano3nninf  13215  nninfalllemn  13216  nninfalllem1  13217  nninfall  13218  nninfsellemdc  13220  nninfsellemeq  13224  nninfsellemqall  13225  nninfsellemeqinf  13226  nninfsel  13227  nninfomni  13229  exmidsbthr  13232  qdencn  13236  refeq  13237  isomninnlem  13239
  Copyright terms: Public domain W3C validator