Theorem opreq1 3953

Description: Equality theorem for operation value.

Assertion

Ref	Expression
opreq1	|- (A = B -> (AFC) = (BFC))

Proof of Theorem opreq1

Step	Hyp	Ref	Expression
1		opeq1 2478	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	fveq2d 3713	. 2 |- (A = B -> (F` <.A, C>.) = (F` <.B, C>.))
3		df-opr 3950	. 2 |- (AFC) = (F` <.A, C>.)
4		df-opr 3950	. 2 |- (BFC) = (F` <.B, C>.)
5	2, 3, 4	3eqtr4g 1523	1 |- (A = B -> (AFC) = (BFC))

Syntax hints:   -> wi 3   = wceq 953  <.cop 2401  ` cfv 3172  (class class class)co 3948

This theorem is referenced by:  opreq12 3955  opreq1i 3956  opreq1d 3960  rcla4eopr 3975  foprcl 4000  caoprcl 4038  caoprcom 4039  caoprass 4040  caoprcan 4041  caoprord 4042  caoprdistr 4045  caoprmo 4056  elrnoprabg 4108  oe0 4145  oev2 4146  omsuc 4149  oesuc 4150  oecl 4156  om0r 4158  om1r 4161  oe1m 4163  oawordeu 4173  omord 4183  omwordi 4186  om00 4190  odi 4194  omass 4195  oewordi 4202  oewordri 4203  oelim2 4206  nnacom 4217  nnmsucr 4224  nnmcom 4225  nneob 4239  th3qlem2 4299  th3q 4301  ecoprcom 4303  ecoprass 4304  ecoprdi 4305  map0 4328  mapdom2 4474  unfilem3 4526  addcmpblnq 5024  addclpq 5030  mulclpq 5032  mulidpq 5041  recmulpq 5042  ltapq 5048  ltmpq 5049  ltexpq 5052  genpv 5074  genpass 5084  distrlem4pr 5102  prlem934a 5109  prlem934b 5110  ltexprlem7 5120  prlem936 5127  mulcmpblnrlem 5154  addclsr 5164  mulclsr 5165  0idsr 5178  1idsr 5179  00sr 5180  ltasr 5181  recexsrlem 5184  mulgt0sr 5186  suppsr 5194  suppsr2 5195  supsrlem4 5200  supsr 5203  addcnsr 5225  mulcnsr 5226  axaddopr 5237  axmulopr 5238  axaddrcl 5244  axmulrcl 5246  ax0id 5253  ax1id 5254  axrnegex 5255  axrrecex 5256  axcnre 5258  pre-axltadd 5261  pre-axmulgt0 5262  cnegextlem1 5317  cnegextlem2 5318  cnegext 5320  addcan 5323  addcant 5324  negeu 5327  subvalt 5329  subclt 5339  subaddt 5347  negsubt 5354  subid1t 5368  mul01t 5415  mulneg1t 5423  mul2negt 5426  negdit 5427  addge0 5573  addgegt0 5574  add20 5576  mulge0 5581  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  lesubaddt 5603  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  lesub0t 5651  mulge0t 5652  recext 5657  mulcan 5659  mulcant2 5660  mulcant 5661  mul0or 5663  mul0ort 5665  receu 5670  divval 5673  divmulz 5675  divmult 5676  divclt 5681  divcan1t 5689  divcan2t 5690  divrect 5702  divdirt 5713  divcan3z 5716  divcan3t 5718  div11t 5721  div1t 5729  redivclt 5756  prodgt0 5775  ltmul1i 5777  prodgt0t 5782  prodge0t 5784  ltmul1t 5786  ltdiv1t 5805  ltmuldivt 5817  peano2nn 5883  nnleltp1t 5901  nnsub 5903  nnsubt 5904  nndivt 5906  halfpost 5983  nn0addclt 6067  nn0mulcl 6069  nn0mulclt 6070  nn0ltp1let 6074  nn0subt 6108  elnn0nn 6118  zltp1let 6128  nneo 6144  nneot 6145  zeot 6146  zneo 6147  zneoOLD 6148  dfuz 6150  uzindOLD 6156  nn0ind-raph 6162  flleltt 6175  flbit 6184  monoord 6231  om2uzsuc 6233  om2uzran 6237  seq1lem1 6246  seq1rn2 6258  shftvalt 6283  seq1shftid 6293  icoshftf1oi 6342  icoshftf1olem 6343  icoun 6346  snunioo 6348  uzind4s 6384  uzind4s2 6385  seq0fval 6467  seqzfval 6469  seqzrn2 6488  expp1t 6506  expcllem 6507  1expt 6516  expge0t 6522  expge1t 6524  mulexpt 6525  recexpt 6526  expaddt 6527  expmult 6528  expwordit 6534  expword2it 6536  exple1t 6538  sq0t 6550  sq11t 6560  sqge0t 6564  sumsqne0 6565  sq0i 6567  sqlecant 6572  sqeqort 6580  binom2t 6581  sq01t 6582  discrlem2 6587  discrlem3 6588  discrlem 6589  nn0opth2t 6598  sqrmul 6635  sqrsqt 6652  sqr2irrlem2 6655  sqr2irrlem3 6656  sqr2irrlem5 6658  crulem 6666  crut 6668  creur 6673  creui 6674  replimt 6692  reim0bt 6712  rereb 6715  readdt 6740  imaddt 6743  cjaddt 6747  cjmult 6748  cjexpt 6752  abs00 6777  absmult 6793  absdivt 6795  absexpt 6803  cjdivt 6827  abssubt 6832  abstrit 6835  abs1m 6841  recant 6842  abs3lemt 6844  facp1t 6873  faclbnd 6882  faclbnd3 6884  faclbnd4lem1 6885  faclbnd4lem2 6886  faclbnd4lem3 6887  faclbnd4lem4 6888  bcvalt 6895  bcpasc2t 6906  bcpasc 6907  bcpasct 6908  bccl2t 6909  fsump1slem 6950  fsumsplit 6958  fsumadd 6960  fsumconst 6976  serzrelem 6999  binomlem2 7005  binomlem6 7009  binom 7010  bcxmas 7014  climconst 7031  climshft 7041  iserzshft2 7044  climmulc2 7065  ser1const 7107  cvgcmp3cetlem1 7124  fnsmnt 7161  expcnvlem5 7166  expcnvlem6 7167  geoser 7169  geolim 7172  geolim1 7174  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem4 7188  fsum0diaglem2 7192  fsum0diag 7193  fsum0diag2 7194  fsum0diag4 7196  mulc1cncf 7214  ivthlem8 7223  ivthlem8OLD 7232  efcltlem2 7247  efseq1ex 7248  efvalt 7250  ef0lem 7252  efaddt 7309  efne0t 7311  efexpt 7314  eftlext 7320  ef1tlub 7324  ef01tllem1 7325  ef01tllem2 7326  ef01tlub 7327  absef01tlub 7329  eirr 7335  ef4pt 7341  efcnlem4 7362  sinaddt 7395  cosaddt 7396  demoivre 7426  acdc2lem1 7430  acdc5lem1 7433  infpn2 7452  ruclem4 7456  ruclem25 7477  ruclem29 7481  ruclem32 7484  retopbas 7597  meteq0 7751  mettri2 7752  mettri4 7753  blval 7777  blelrn 7788  metcni 7833  blssioo 7852  tgioolem 7853  metcnp4lem2 7903  metcnp4 7904  bcthlem15 7947  bcthlem16 7948  bcthlem17 7949  bcthlem18 7950  isgrpi 7976  grpass 7981  grpidinvlem1 7982  grpidinvlem2 7983  grpidinvlem3 7984  grpidinvlem4 7985  grpideu 7987  grpidinv2 7994  grprcan 7997  grpinveu 7998  grpinv 8003  grpinvid2 8007  isgrp2i 8011  grpdivval 8017  grplactfval 8032  ablcom 8039  issubgilem 8058  grpsn 8061  ablsn 8062  cnid 8064  mulid 8069  ghgrpilem1 8070  ghgrpilem3 8072  ghgrpilem4 8073  ghgrpi 8074  ringid 8082  ringdi 8083  ringdir 8084  ringass 8085  cnring 8099  ringsn 8100  vcdi 8108  vcdir 8109  vcass 8110  nvmul0or 8212  nvs 8229  nvtri 8237  sqcn 8270  va1cnlem 8279  sm1cnilem 8281  ipval 8287  ip1cnilem3 8309  ip1cnilem4 8310  ip1cnilem6 8312  lnolin 8349  bloval 8373  nmlno0 8387  isblo3i 8392  blo3i 8393  blocnilem 8395  phpar2 8413  phpar 8414  ipdiri 8420  ipasslem1 8421  ipasslem5 8425  ipasslem6 8426  ipasslem8 8428  ipasslem9 8429  ipasslem11 8431  ipassi 8432  siilem2 8443  sii 8445  ipblnfi 8447  ip2eqi 8448  ajfun 8452  minveclem36 8511  htthlem2 8551  sincolem 8584  sincosq1eq 8626  efifolem2 8638  efifolem3 8639  shftefif1olem 8661  shftefif1olemOLD 8662  hvsubvalt 8807  hvmul0ort 8815  hvsubsub4t 8848  hvsubeq0 8851  hvaddcan 8853  hvnegdit 8855  hvsubeq0t 8856  hvaddcant 8858  hvsubaddt 8865  hiidge0t 8885  his6t 8886  hial0 8889  hial02 8890  hial2eqt 8893  normlem6 8902  normlem7tALT 8906  bcseq 8907  normlem9at 8908  normgt0tOLD 8914  normgt0t 8915  normsub0t 8924  norm-iit 8926  norm-iiit 8928  normsubt 8931  normpytht 8933  norm3dift 8938  norm3lemt 8940  norm3adift 8941  normpart 8943  polidt 8947  hilid 8949  bcst 8969  shaddclt 9006  shaddcltOLD 9007  shmulclt 9008  shmulcltOLD 9009  hlimcaui 9027  ocelt 9070  occllem2 9090  occllem8 9096  projlem7 9108  projlem8 9109  projlem10 9111  projlem15 9116  projlem16 9117  projlem17 9118  projlem20 9121  pjthlem8 9141  pjthlem9 9142  pjthlem12 9145  pjth 9148  pjtheu 9150  pjeq2t 9156  omlsi 9160  pjpj0 9170  shsclt 9197  shslejt 9265  shlubt 9269  chj0t 9335  chlejb1t 9350  chnlet 9352  chjasst 9371  ledit 9378  h1de2ctlem 9394  elspansn2t 9406  spansncol 9407  spansneleq 9409  spansneleqOLD 9410  normcant 9416  pjspansnt 9417  h1datom 9421  hommvalt 9429  hfmmvalt 9432  cmbr3 9460  osumlem5 9499  osumlem8 9502  osumt 9505  spansnjt 9509  spansncvt 9515  5oalem2 9517  pjssge0 9544  pjadjt 9547  pjaddt 9548  pjsubt 9550  pjmult 9551  pjcjt2 9554  hosubclt 9616  hoaddcomt 9617  hoaddasst 9625  hocsubdirt 9628  hoaddid1t 9634  ho0subt 9640  honegsubt 9642  hosubeq0 9669  adjsymt 9676  eigre 9677  eigret 9678  eigpos 9679  eigorth 9680  eigortht 9681  specvalt 9741  lnoplt 9754  unopt 9755  hmopt 9762  lnfnlt 9771  adjt 9773  bravalvalt 9784  kbvalvalt 9794  kbpjt 9796  hoddit 9830  lnopeq0lem2 9846  lnopunilem1 9850  lnopunilem2 9851  lnopuni 9852  lnophm 9858  lnopcon 9878  lnopcnbdt 9880  lnfncon 9905  lnfncnbdt 9907  nlelch 9909  riesz4 9911  riesz1t 9913  cnlnadjlem2 9916  cnlnadjlem5 9919  cnlnadjlem8 9922  branmfnt 9951  leopg 9967  hstel2t 10056  hst1ht 10064  stjt 10072  strlem3a 10089  mdit 10132  mdbr3 10134  mdbr4 10135  dmdbrt 10136  dmdmdt 10137  dmdi4 10143  mdsl1 10156  cvmd 10159  mdslmd1lem3 10162  mdslmd1lem4 10163  mdslmd1 10164  superpos 10189  cvexcht 10209  atcv0eq 10214  atcv1t 10215  mdsymlem2 10239  sumdmdlem2 10253  cdjreu 10264  cdj1 10265  cdj3lem1 10266  cdj3lem2 10267  cdj3lem2b 10269  cdj3lem3b 10272  cdj3 10273  abs2sqlet 10279  abs2sqltt 10280  ghomgrpilem1 10290  ghomlin 10298  ghomf1olem 10301  elgiso 10303  cayleylem2 10317  cayleythlem 10320  hmph 10411  hmeogrp 10425  trran 10480  trnij 10481  cnvtr 10482  1ded 10515  domcmpd 10523  codcmpd 10524  cmpasso 10550  cmpidb 10552  ismonb 10580  ispgrag 10615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950

Copyright terms: Public domain