Theorem opreq1 4026

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq1

Step	Hyp	Ref	Expression
1		opeq1 2541	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	fveq2d 3785	. 2 |- (A = B -> (F` <.A, C>.) = (F` <.B, C>.))
3		df-opr 4023	. 2 |- (AFC) = (F` <.A, C>.)
4		df-opr 4023	. 2 |- (BFC) = (F` <.B, C>.)
5	2, 3, 4	3eqtr4g 1578	1 |- (A = B -> (AFC) = (BFC))

Syntax hints:   -> wi 3   = wceq 997  <.cop 2463  ` cfv 3239  (class class class)co 4021

This theorem is referenced by:  opreq12 4028  opreq1i 4029  opreq1d 4033  rcla4eopr 4048  foprcl 4073  caoprcl 4110  caoprcom 4111  caoprass 4112  caoprcan 4113  caoprord 4114  caoprdistr 4117  caoprmo 4128  elrnoprabg 4182  oe0 4219  oev2 4220  omsuc 4223  oesuc 4224  oecl 4230  om0r 4232  om1r 4235  oe1m 4237  oawordeu 4247  omord 4257  omwordi 4260  om00 4264  odi 4268  omass 4269  oewordi 4276  oewordri 4277  oelim2 4280  nnacom 4291  nnmsucr 4298  nnmcom 4299  nneob 4313  th3qlem2 4376  th3q 4378  ecoprcom 4380  ecoprass 4381  ecoprdi 4382  map0 4405  mapdom2 4559  unfilem3 4613  addcmpblnq 5117  addclpq 5123  mulclpq 5125  mulidpq 5134  recmulpq 5135  ltapq 5141  ltmpq 5142  ltexpq 5145  genpv 5167  genpass 5177  distrlem4pr 5195  prlem934a 5202  prlem934b 5203  ltexprlem7 5213  prlem936 5220  mulcmpblnrlem 5247  addclsr 5257  mulclsr 5258  0idsr 5271  1idsr 5272  00sr 5273  ltasr 5274  recexsrlem 5277  mulgt0sr 5279  suppsr 5287  suppsr2 5288  supsrlem4 5293  supsr 5296  addcnsr 5318  mulcnsr 5319  axaddopr 5330  axmulopr 5331  axaddrcl 5337  axmulrcl 5339  ax0id 5346  ax1id 5347  axrnegex 5348  axrrecex 5349  axcnre 5351  pre-axltadd 5354  pre-axmulgt0 5355  cnegexlem1 5410  cnegexlem2 5411  cnegex 5413  addcani 5416  addcan 5417  negeui 5420  subval 5422  subcl 5432  subadd 5440  negsub 5447  subid1 5461  mul01 5508  mulneg1 5516  mul2neg 5519  negdi 5520  addge0i 5664  addgegt0i 5665  add20i 5667  mulge0i 5672  ltadd1 5688  leadd1 5690  ltsubadd 5692  lesubadd 5694  lt2add 5708  le2add 5709  addgt0 5712  addgegt0 5713  addge0 5715  lesub0 5743  mulge0 5744  recex 5749  mulcani 5751  mulcaniOLD 5752  mulcant2i 5753  mulcant2iOLD 5754  mulcan 5755  mulcanOLD 5756  mul0ori 5759  mul0or 5761  receui 5766  divvali 5769  divmulzi 5771  divmul 5772  divmulOLD 5773  divcl 5780  divcan1 5788  divrec 5801  divdir 5813  divdirOLD 5814  divcan3zi 5817  divcan3 5819  div11 5822  div1 5830  redivcl 5858  prodgt0i 5877  ltmul1ii 5879  prodgt0 5884  prodge0 5886  ltmul1 5888  ltdiv1 5907  ltdiv1OLD 5908  ltmuldiv 5921  ltmuldivOLD 5922  peano2nn 5995  nnleltp1 6015  nnsubi 6017  nnsub 6018  nndiv 6020  halfpos 6097  nn0addcl 6202  nn0mulcli 6204  nn0mulcl 6205  nn0ltp1le 6209  nn0sub 6243  elnn0nn 6253  zltp1le 6263  zdiv 6270  nneoi 6282  nneo 6283  zeo 6284  zneo 6285  dfuzi 6287  uzindOLD 6293  nn0ind-raph 6299  fllelt 6339  flbi 6352  modval 6372  modadd1 6380  monoord 6381  icoshftf1oii 6435  icoshftf1olem 6436  icoun 6439  snunioo 6441  uzind4s 6478  uzind4s2 6479  om2uzsuci 6554  om2uzrani 6558  seq1lem1 6568  seq1rn2 6580  shftval 6605  seq1shftid 6615  seq0fval 6624  seqzfval 6626  seqzrn2 6645  expp1 6663  expcllem 6664  1exp 6673  expge0 6680  expge1 6682  mulexp 6683  recexp 6684  expadd 6685  expmul 6686  expwordi 6692  expword2i 6694  exple1 6696  sq11 6718  sqge0 6722  sumsqne0i 6723  sq0i 6725  sqlecan 6730  sqeqor 6738  binom2 6739  sq01 6740  discrlem2 6747  discrlem3 6748  discrlem 6749  nn0opth2 6758  sqrmuli 6795  sqrsq 6812  sqr2irrlem2 6815  sqr2irrlem3 6816  sqr2irrlem5 6818  crulem 6826  cru 6828  creur 6832  creui 6833  replim 6851  readd 6895  imadd 6898  cjadd 6902  cjmul 6903  cjexp 6907  abs00i 6932  absmul 6948  absdiv 6950  absexp 6958  cjdiv 6979  abssub 6984  abstri 6988  abs1mi 6994  recan 6995  abs3lem 6997  facp1 7026  faclbnd 7035  faclbnd3 7037  faclbnd4lem1 7038  faclbnd4lem2 7039  faclbnd4lem3 7040  faclbnd4lem4 7041  bcval 7048  bcpasc2 7058  bcpasci 7059  bcpasc 7060  bccl2 7061  fsump1slem 7102  fsumspl 7110  fsumadd 7112  fsumcons 7128  serzrelem 7151  binomlem2 7157  binomlem6 7161  binomi 7162  bcxmas 7166  climconsti 7184  climshfti 7194  iserzshft2i 7197  climmulc2 7219  ser1consti 7261  cvgcmp3cetlem1 7278  arisumi 7316  expcnvlem5 7321  expcnvlem6 7322  geoseri 7324  geolim 7327  geolim1 7329  cvgratlem1ALT 7337  cvgratlem1 7340  cvgratlem4 7343  fsum0diaglem2 7347  fsum0diag 7348  fsum0diag2 7349  fsum0diag4 7351  mulc1cncf 7369  ivthlem8 7378  efcltlem2 7395  efseq1ex 7396  efval 7398  ef0lem 7400  efadd 7457  efne0 7459  efexp 7462  eftlex 7468  ef1tlubi 7472  ef01tllem1 7473  ef01tllem2 7474  ef01tllem2OLD 7475  ef01tlubi 7476  absef01tlubi 7478  eirr 7484  ef4p 7491  efcnlem4 7513  sinadd 7544  cosadd 7545  demoivre 7576  acdc2lem1 7580  acdc5lem1 7583  infpn2 7601  ruclem4 7605  ruclem25 7626  ruclem29 7630  ruclem32 7633  retopbas 7740  meteq0 7897  mettri2 7898  mettri4 7899  blval 7922  blelrn 7933  metcni 7979  blssioo 7998  tgioolem 7999  metcnp4lem2 8054  metcnp4 8055  bcthlem15 8098  bcthlem16 8099  bcthlem17 8100  bcthlem18 8101  isgrpi 8127  grpass 8132  grpidinvlem1 8133  grpidinvlem2 8134  grpidinvlem3 8135  grpidinvlem4 8136  grpideu 8138  grpidinv2 8144  grprcan 8147  grpinveu 8148  grpinv 8153  grpinvid2 8157  isgrp2i 8160  grpdivval 8166  grplactfval 8180  ablcom 8187  issubgilem 8205  grpsn 8208  ablsn 8209  cnid 8211  mulid 8216  ghgrpilem1 8217  ghgrpilem3 8219  ghgrpilem4 8220  ghgrpi 8221  ringid 8229  ringdi 8230  ringdir 8231  ringass 8232  cnring 8246  ringsn 8247  vcdi 8255  vcdir 8256  vcass 8257  nvmul0or 8356  nvs 8374  nvtri 8382  sqcn 8419  va1cnlem 8429  sm1cnilem 8431  ipval 8437  ip1cnilem3 8459  ip1cnilem4 8460  ip1cnilem6 8462  lnolin 8499  bloval 8525  nmlno0 8539  isblo3i 8545  blo3i 8546  blocnilem 8548  phpar2 8566  phpar 8567  ipdiri 8573  ipasslem1 8574  ipasslem5 8578  ipasslem6 8579  ipasslem8 8581  ipasslem9 8582  ipasslem11 8584  ipassi 8585  siilem2 8596  sii 8598  ipblnfi 8600  ip2eqi 8601  ajfun 8605  minveclem36 8664  htthlem2 8705  sincolem 8748  sincosq1eq 8792  efifolem2 8806  efifolem3 8807  shftefif1olem 8824  hvsubval 8969  hvmul0or 8977  hvsubsub4 9010  hvsubeq0i 9013  hvaddcani 9015  hvnegdi 9017  hvsubeq0 9018  hvaddcan 9020  hvsubadd 9027  hiidge0 9047  his6 9048  hial0 9051  hial02 9052  hial2eq 9055  normlem6 9064  normlem7tALT 9068  bcseqi 9069  normlem9at 9070  normgt0OLD 9076  normgt0 9077  normsub0 9086  norm-ii 9088  norm-iii 9090  normsub 9093  normpyth 9095  norm3dif 9100  norm3lemt 9102  norm3adifi 9103  normpar 9105  polid 9109  hilid 9111  bcs 9131  shaddcl 9168  shaddclOLD 9169  shmulcl 9170  shmulclOLD 9171  hlimcauii 9189  ocel 9237  occllem2 9257  occllem8 9263  projlem7 9275  projlem8 9276  projlem10 9278  projlem15 9283  projlem16 9284  projlem17 9285  projlem20 9288  pjthlem8 9309  pjthlem9 9310  pjthlem12 9313  pjthi 9316  pjtheui 9318  pjeq2 9324  omlsii 9328  pjpj0i 9338  shscl 9365  shslej 9433  shlub 9437  chj0 9503  chlejb1 9518  chnle 9520  chjass 9539  ledi 9546  h1de2ctlem 9561  elspansn2 9573  spansncol 9574  spansneleq 9576  normcan 9582  pjspansn 9583  h1datomi 9587  hommval 9595  hfmmval 9598  cmbr3i 9626  osumlem5 9665  osumlem8 9668  osum 9671  spansnj 9675  spansncv 9681  5oalem2 9683  pjssge0ii 9710  pjadji 9713  pjaddi 9714  pjsubi 9716  pjmuli 9717  pjcjt2 9720  hosubcl 9782  hoaddcom 9783  hoaddass 9791  hocsubdir 9794  hoaddid1 9800  ho0sub 9806  honegsub 9808  hosubeq0i 9835  adjsym 9842  eigrei 9843  eigre 9844  eigposi 9845  eigorthi 9846  eigorth 9847  specval 9907  lnopl 9921  unop 9922  hmop 9929  lnfnl 9938  adj1 9940  bravalval 9951  kbvalval 9961  kbpj 9963  hoddi 9998  lnopeq0lem2 10014  lnopunilem1 10018  lnopunilem2 10019  lnopunii 10020  lnophmi 10026  lnopconi 10046  lnopcnbd 10048  lnfnconi 10073  lnfncnbd 10075  nlelchi 10077  riesz4i 10079  riesz1 10081  cnlnadjlem2 10084  cnlnadjlem5 10087  cnlnadjlem8 10090  branmfn 10121  leopg 10138  hstel2 10230  hst1h 10238  stj 10246  strlem3a 10263  mdi 10306  mdbr3 10308  mdbr4 10309  dmdbr 10310  dmdmd 10311  dmdi4 10318  dmdbr5 10319  mdsl1i 10332  cvmdi 10335  mdslmd1lem3 10338  mdslmd1lem4 10339  mdslmd1i 10340  superpos 10365  cvexch 10385  atcv0eq 10390  atcv1 10391  mdsymlem2 10415  sumdmdlem2 10430  cdjreui 10443  cdj1i 10444  cdj3lem1 10445  cdj3lem2 10446  cdj3lem2b 10448  cdj3lem3b 10451  cdj3i 10452  abs2sqlet 10459  abs2sqltt 10460  ghomgrpilem1 10470  ghomlin 10478  ghomf1olem 10481  elgiso 10483  cayleylem2 10495  cayleythlem 10498  hmph 10618  hmeogrp 10632  trran 10718  trnij 10719  cnvtr 10720  1ded 10753  domcmpd 10761  codcmpd 10762  cmpasso 10788  cmpidb 10790  ismonb 10820  isepib2 10832  ispgrag 10863

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-xp 3241  df-cnv 3243  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fv 3255  df-opr 4023

Copyright terms: Public domain