Theorem opreq1 4889

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq1

Step	Hyp	Ref	Expression
1		opeq1 3158	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	fveq2d 4685	. 2 |- (A = B -> (F` <.A, C>.) = (F` <.B, C>.))
3		df-opr 4886	. 2 |- (AFC) = (F` <.A, C>.)
4		df-opr 4886	. 2 |- (BFC) = (F` <.B, C>.)
5	2, 3, 4	3eqtr4g 1953	1 |- (A = B -> (AFC) = (BFC))

Syntax hints:   -> wi 3   = wceq 1298  <.cop 3046  ` cfv 3998  (class class class)co 4884

This theorem is referenced by:  opreq12 4891  opreq1i 4892  opreq1d 4897  rcla4eopr 4915  foprcl 4944  caoprcl 4985  caoprcom 4986  caoprass 4987  caoprcan 4988  caoprord 4989  caoprdistr 4992  caoprmo 5003  elrnoprabg 5066  curry2 5078  curry2val 5080  oe0 5206  oev2 5207  omsuc 5210  oesuc 5211  oecl 5218  oeclOLD 5219  om0r 5221  om1r 5224  oe1m 5226  oawordeu 5237  omord 5247  omwordi 5250  om00 5254  odi 5258  omass 5259  oewordi 5266  oewordri 5267  oelim2 5270  oeoalem 5271  oeoa 5272  oeoelem 5273  oeoe 5274  nnacom 5288  nnmsucr 5295  nnmsucrOLD 5296  nnmcom 5297  nnmcomOLD 5298  nneob 5312  th3qlem2 5374  th3q 5376  ecoprcom 5378  ecoprass 5379  ecoprdi 5380  map0 5403  mapdom2 5588  unfilem3 5643  cdaung 6071  cdaeng 6074  nnacda 6088  addcmpblnq 6204  addclpq 6210  mulclpq 6212  mulidpq 6221  recmulpq 6222  ltapq 6228  ltmpq 6229  ltexpq 6232  genpv 6254  genpass 6264  distrlem4pr 6282  prlem934a 6289  prlem934b 6290  ltexprlem7 6300  prlem936 6307  mulcmpblnrlem 6334  addclsr 6344  mulclsr 6345  0idsr 6358  1idsr 6359  00sr 6360  ltasr 6361  recexsrlem 6364  mulgt0sr 6366  suppsr 6374  suppsr2 6375  supsrlem4 6380  supsr 6383  addcnsr 6405  mulcnsr 6406  axaddopr 6417  axmulopr 6418  axaddrcl 6425  axmulrcl 6427  ax0id 6434  ax1id 6435  axrnegex 6436  axrrecex 6437  axcnre 6439  pre-axltadd 6442  pre-axmulgt0 6443  cnegexlem1 6499  cnegexlem2 6500  cnegex 6502  addcani 6505  addcaniOLD 6506  addcan 6507  negeui 6510  subval 6512  subcl 6524  subadd 6532  negsub 6540  subid1 6556  mul01 6606  mulneg1 6615  mul2negOLD 6619  negdi 6620  addge0iOLD 6778  addgegt0i 6779  addgegt0iOLD 6780  add20i 6782  mulge0i 6787  ltadd1 6806  leadd1 6808  ltsubadd 6810  lesubadd 6812  lt2add 6827  le2add 6828  addgt0OLD 6832  addgegt0OLD 6834  addge0OLD 6838  lesub0 6867  mulge0 6868  mulge0OLD 6869  recex 6876  mulcani 6878  mulcant2i 6879  mulcan 6880  mul0ori 6882  mul0or 6884  receui 6890  divvali 6893  divmulzi 6895  divmul 6896  divcl 6901  divcan1 6909  divrec 6922  divdir 6933  divcan3zi 6936  divcan3 6938  div11 6941  div1 6949  redivcl 6978  prodgt0i 6997  ltmul1ii 6999  prodgt0 7004  prodge0 7006  ltmul1 7008  ltdiv1 7031  ltdiv1OLD 7032  ltmuldiv 7045  ltmuldivOLD 7046  peano2nn 7118  nnleltp1 7138  nnsubi 7140  nnsub 7141  nndiv 7143  halfpos 7222  nn0addcl 7329  nn0mulcli 7331  nn0mulcl 7332  nn0ltp1le 7336  nn0sub 7370  elnn0nn 7380  zltp1le 7390  zdiv 7397  nneoi 7409  nneo 7410  zeo 7411  zneo 7412  dfuzi 7414  uzindOLD 7420  nn0ind-raph 7426  fllelt 7467  flbi 7480  modval 7501  modadd1 7518  modmul1 7519  monoord 7523  icoshftf1oii 7578  icoshftf1olem 7579  icoun 7582  snunioo 7584  uzind4s 7621  uzind4s2 7622  om2uzsuci 7707  om2uzrani 7711  seq1lem1 7722  seq1rn2 7734  shftval 7759  seq1shftid 7769  seq0fval 7778  seqzfval 7780  seqzrn2 7799  expp1 7817  expcllem 7818  1exp 7827  expge0 7833  expge1 7835  mulexp 7836  exprec 7837  exprecOLD 7838  expadd 7839  expmul 7840  expwordi 7848  expword2i 7850  exple1 7852  sq11 7874  sqge0 7878  sumsqne0i 7879  sq0i 7881  sqlecan 7887  sqeqor 7895  binom2 7896  sq01 7897  discrlem2 7907  discrlem3 7908  discrlem 7909  nn0opth2 7918  sqrmuli 7955  sqrsq 7972  sqr2irrlem2 7975  sqr2irrlem3 7976  sqr2irrlem5 7978  crulem 7986  cru 7988  creur 7992  creui 7993  replim 8011  readd 8055  imadd 8058  cjadd 8062  cjmul 8063  cjexp 8067  abs00i 8093  absmul 8109  absdiv 8111  absexp 8119  cjdiv 8141  abssub 8146  abstri 8150  abs1mi 8156  recan 8157  abs3lem 8159  facp1 8188  faclbnd 8197  faclbnd3 8199  faclbnd4lem1 8200  faclbnd4lem2 8201  faclbnd4lem3 8202  faclbnd4lem4 8203  bcval 8210  bcpasc2 8220  bcpasci 8221  bcpasc 8222  bccl2 8223  fsump1slem 8272  fsumsplit 8280  fsumadd 8282  fsumconst 8298  serzrelem 8321  binomlem2 8327  binomlem6 8331  binomi 8332  bcxmas 8336  climconsti 8354  climshfti 8364  iserzshft2i 8367  climmulc2 8389  ser1consti 8431  cvgcmp3cetlem1 8449  arisumi 8487  expcnvlem5 8492  expcnvlem6 8493  geoseri 8496  geolim 8499  geolim1 8501  cvgratlem1ALT 8509  cvgratlem1 8512  cvgratlem4 8515  fsum0diaglem2 8519  fsum0diag 8520  fsum0diag2 8521  fsum0diag4 8523  mulc1cncf 8541  ivthlem8 8550  efcltlem2 8567  efseq1ex 8568  efval 8570  ef0lem 8572  efadd 8629  efne0 8631  efexp 8634  eftlex 8640  ef1tlubi 8644  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  ef01tlubi 8648  absef01tlubi 8650  eirr 8656  ef4p 8665  efcnlem4 8687  sinadd 8718  cosadd 8719  demoivre 8752  acdc2lem1 8757  acdc5lem1 8760  infpn2 8778  ruclem4 8782  ruclem25 8803  ruclem29 8807  ruclem32 8810  retopbas 8925  meteq0 9089  mettri2 9090  mettri4 9091  blval 9114  blelrn 9125  metcni 9172  blssioo 9191  tgioolem 9192  metcnp4lem2 9247  metcnp4 9248  bcthlem15 9291  bcthlem16 9292  bcthlem17 9293  bcthlem18 9294  isgrpi 9322  grpass 9327  grpidinvlem1 9328  grpidinvlem2 9329  grpidinvlem3 9330  grpidinvlem4 9331  grpideu 9333  grpsn 9340  grpidinv2 9344  grprcan 9347  grpinveu 9348  grpinv 9353  grpinvid2 9357  isgrp2i 9360  grpdivval 9367  gxoprval 9380  gx1 9385  gxnn0suc 9387  gxnn0add 9397  gxnn0mul 9400  gxmodid 9402  grplactfval 9404  ablcom 9411  gxdi 9422  issubgilem 9430  ablsn 9433  cnid 9435  addinv 9436  mulid 9440  ghgrpilem1 9441  ghgrpilem3 9443  ghgrpilem4 9444  ghgrpi 9445  gaass 9459  ringid 9469  ringideu 9470  ringdi 9471  ringdir 9472  ringass 9473  cnring 9489  ringsn 9490  vcdi 9503  vcdir 9504  vcass 9505  nvmul0or 9604  nvs 9622  nvtri 9630  sqcn 9674  va1cnlem 9684  sm1cnilem 9686  ipval 9692  ip1cnilem3 9714  ip1cnilem4 9715  ip1cnilem6 9717  lnolin 9754  bloval 9781  nmlno0 9795  isblo3i 9801  blo3i 9802  blocnilem 9804  phpar2 9823  phpar 9824  ipdiri 9830  ipasslem1 9831  ipasslem5 9835  ipasslem6 9836  ipasslem8 9838  ipasslem9 9839  ipasslem11 9841  ipassi 9842  siilem2 9853  sii 9855  ipblnfi 9857  ip2eqi 9858  ajfun 9862  minveclem36 9925  htthlem2 9968  isla 10010  sincolem 10014  sincosq1eq 10059  efifolem2 10077  efifolem3 10078  shftefif1olem 10095  ghomlin 10196  hmph 10241  subtopmet 10256  exidu1 10373  cmpidelt 10376  hvsubval 10518  hvmul0or 10526  hvsubsub4 10559  hvsubeq0i 10562  hvaddcani 10564  hvnegdi 10566  hvsubeq0 10567  hvaddcan 10569  hvsubadd 10577  hiidge0 10597  his6 10598  hial0 10601  hial02 10602  hial2eq 10605  normlem6 10614  normlem7tALT 10618  bcseqi 10619  normlem9at 10620  normgt0OLD 10626  normgt0 10627  normsub0 10636  norm-ii 10638  norm-iii 10640  normsub 10643  normpyth 10645  norm3dif 10650  norm3lemt 10652  norm3adifi 10653  normpar 10655  polid 10659  hilid 10661  bcs 10681  shaddcl 10718  shaddclOLD 10719  shmulcl 10720  shmulclOLD 10721  hlimcauii 10739  ocel 10787  occllem2 10807  occllem8 10813  projlem7 10825  projlem8 10826  projlem10 10828  projlem15 10833  projlem16 10834  projlem17 10835  projlem20 10838  pjthlem8 10859  pjthlem9 10860  pjthlem12 10863  pjthi 10866  pjtheui 10868  pjeq2 10874  omlsii 10878  pjpj0i 10888  shscl 10915  shslej 10983  shlub 10987  chj0 11053  chlejb1 11068  chnle 11070  chjass 11089  ledi 11096  h1de2ctlem 11111  elspansn2 11123  spansncol 11124  spansneleq 11126  normcan 11132  pjspansn 11133  h1datomi 11137  hommval 11145  hfmmval 11148  cmbr3i 11176  osumlem5 11217  osumlem8 11220  osum 11223  spansnj 11227  spansncv 11233  5oalem2 11235  pjssge0ii 11262  pjadji 11265  pjaddi 11266  pjsubi 11268  pjmuli 11269  pjcjt2 11272  hosubcl 11336  hoaddcom 11337  hoaddass 11345  hocsubdir 11348  hoaddid1 11354  ho0sub 11360  honegsub 11362  hosubeq0i 11389  adjsym 11396  eigrei 11397  eigre 11398  eigposi 11399  eigorthi 11400  eigorth 11401  specval 11461  lnopl 11475  unop 11476  hmop 11483  lnfnl 11492  adj1 11494  bravalval 11505  kbvalval 11515  kbpj 11517  hoddi 11552  lnopeq0lem2 11568  lnopunilem1 11572  lnopunilem2 11573  lnopunii 11574  lnophmi 11580  lnopconi 11600  lnopcnbd 11602  lnfnconi 11627  lnfncnbd 11629  nlelchi 11631  riesz4i 11633  riesz1 11635  cnlnadjlem2 11638  cnlnadjlem5 11641  cnlnadjlem8 11644  branmfn 11675  branmfnOLD 11676  leopg 11693  opsqrlem4 11714  hstel2 11791  hst1h 11799  stj 11807  strlem3a 11824  mdi 11867  mdbr3 11869  mdbr4 11870  dmdbr 11871  dmdmd 11872  dmdi4 11879  dmdbr5 11880  mdsl1i 11893  cvmdi 11896  mdslmd1lem3 11899  mdslmd1lem4 11900  mdslmd1i 11901  superpos 11926  cvexch 11946  atcv0eq 11951  atcv1 11952  mdsymlem2 11976  sumdmdlem2 11991  cdjreui 12004  cdj1i 12005  cdj3lem1 12006  cdj3lem2 12007  cdj3lem2b 12009  cdj3lem3b 12012  cdj3i 12013  abs2sqle 13624  abs2sqlt 13625  ghomgrpilem1 13628  ghomf1olem 13637  elgiso 13639  cayleylem2 13642  cayleythlem 13645  dvds0lem 13665  dvds1lem 13666  dvds2lem 13667  dvdsmulc 13681  dvdsle 13693  divalglem7 13702  divalglem8 13703  gcddvds 13722  gcdcl 13724  gcdaddm 13735  mulgcdlem6 13761  mulgcdlem7 13762  iscst2 14520  nZdef 14527  labss1 14537  labss2 14539  supwval 14629  isdir2 14640  fprodp1slem 14681  iscomb 14690  ridlideq 14695  rzrlzreq 14696  mgmlion 14697  smgrpass2 14701  isppm 14715  seqzp2 14716  mndass2 14721  expm 14725  symgfo 14730  trran2 14757  trooo 14758  trinv 14759  cmprtr 14760  cmprtr2 14761  prsubrtr2 14764  ununr 14769  zerdivemp1 14785  vecax5b 14802  vecax5c 14825  svli2 14826  hmeogrp 14892  usptoplem 14917  istopx 14918  prtoptop 14919  usptop 14920  idtrgrp 14978  invtrgrp 14979  altretop 14997  cntrsetlem 14999  trran 15014  trnij 15015  cnvtr 15016  1ded 15085  domcmpd 15093  codcmpd 15094  cmpasso 15120  cmpidb 15122  dualcat2lem 15129  dualded2lem 15130  dualcat2 15133  ismonb 15159  isepib2 15171  cinvlem3 15178  reconn 15451  ivthALT 15454  eropreu 15733  eroprv 15734  add20 15777  eluzadd 15782  eluzsub 15783  absmod0 15802  seq11g 15804  seq1p1g 15805  seq1seqzg 15808  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  seqpo 15814  incsequz 15815  incsequz2 15816  fsumltisumi 15823  fsumltisum 15824  fsumleisum 15827  iserzshft2 15829  isumshft2 15830  fsumlt1 15831  mettrifi 15847  mettrifi2 15848  geomcau 15849  caushft 15851  addccncf 15883  sub1cncf 15885  txcnoprab 15911  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  bndss 15942  blbnd 15943  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  ismtybndlem 15952  ismtyres 15954  heiborlem1 15955  heiborlem23 15977  heiborlem28 15982  heiborlem30 15984  heiborlem31 15985  heiborlem33 15987  bfplem5 16002  bfplem6 16003  bfplem8 16005  bfplem9 16006  bfplem11 16008  bfp 16009  rrntotbnd 16022  exidres 16031  exidresid 16032  isgrpda 16033  isgrpd 16034  isabld 16036  grpeqdivid 16038  ghomco 16040  phtpycom 16050  phtpycolem1 16051  phtpycolem2 16052  phtpycolem4 16054  phtpyco 16056  isphtpc 16059  reparphtlem1 16063  reparphtlem2 16064  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcoass 16085  pi1gp 16095  isringd 16097  zerdivemp1x 16108  isdivrng2 16111  isdivrng3 16112  rnghomadd 16123  rnghommul 16124  rngisoval 16131  isriscg 16138  iscringd 16147  crngcom 16149  idladdcl 16167  idllmulcl 16168  idlrmulcl 16169  0idl 16173  keridl 16180  smprngpr 16200  prnc 16215  pridlc 16219  dmnnzd 16223  ispgrag 16301  mulvval 16468  latlem 16850  cmtval 16938  omllaw 16964  cmtbr3 16975  hlsuprexch 17033  hlexch 17034  atcvrj0 17065  atltcvr 17072  ps-1 17078  ps2 17079  grplem1 17105  grpidinvlem1NEW 17109  grpidinvlem2NEW 17110  grpidinvlem3NEW 17111  grpidinvlem4NEW 17112  grpideuNEW 17114  isgrpiNEW 17115  grpidinv2NEW 17119  grprcanNEW 17122  grpinveuNEW 17123  grpinvNEW 17128  grpinvid2NEW 17132  ablcomNEW 17138  ringiNEW 17143  ringideuNEW 17146  ringidmlemNEW 17153  divrngidlemNEW 17165  islinei 17221  psubspi2 17229  elpaddn0 17261  elpaddri 17263  elpadd2at 17267  paddasslem12 17292  paddasslem17 17297  pmapjat 17314  osumcl 17375

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-opr 4886

Copyright terms: Public domain