Theorem opreq1 3975

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq1

Step	Hyp	Ref	Expression
1		opeq1 2492	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	fveq2d 3735	. 2 |- (A = B -> (F` <.A, C>.) = (F` <.B, C>.))
3		df-opr 3972	. 2 |- (AFC) = (F` <.A, C>.)
4		df-opr 3972	. 2 |- (BFC) = (F` <.B, C>.)
5	2, 3, 4	3eqtr4g 1534	1 |- (A = B -> (AFC) = (BFC))

Syntax hints:   -> wi 3   = wceq 958  <.cop 2416  ` cfv 3189  (class class class)co 3970

This theorem is referenced by:  opreq12 3977  opreq1i 3978  opreq1d 3982  rcla4eopr 3997  foprcl 4022  caoprcl 4059  caoprcom 4060  caoprass 4061  caoprcan 4062  caoprord 4063  caoprdistr 4066  caoprmo 4077  elrnoprabg 4131  oe0 4168  oev2 4169  omsuc 4172  oesuc 4173  oecl 4179  om0r 4181  om1r 4184  oe1m 4186  oawordeu 4196  omord 4206  omwordi 4209  om00 4213  odi 4217  omass 4218  oewordi 4225  oewordri 4226  oelim2 4229  nnacom 4240  nnmsucr 4247  nnmcom 4248  nneob 4262  th3qlem2 4322  th3q 4324  ecoprcom 4326  ecoprass 4327  ecoprdi 4328  map0 4351  mapdom2 4501  unfilem3 4564  addcmpblnq 5071  addclpq 5077  mulclpq 5079  mulidpq 5088  recmulpq 5089  ltapq 5095  ltmpq 5096  ltexpq 5099  genpv 5121  genpass 5131  distrlem4pr 5149  prlem934a 5156  prlem934b 5157  ltexprlem7 5167  prlem936 5174  mulcmpblnrlem 5201  addclsr 5211  mulclsr 5212  0idsr 5225  1idsr 5226  00sr 5227  ltasr 5228  recexsrlem 5231  mulgt0sr 5233  suppsr 5241  suppsr2 5242  supsrlem4 5247  supsr 5250  addcnsr 5272  mulcnsr 5273  axaddopr 5284  axmulopr 5285  axaddrcl 5291  axmulrcl 5293  ax0id 5300  ax1id 5301  axrnegex 5302  axrrecex 5303  axcnre 5305  pre-axltadd 5308  pre-axmulgt0 5309  cnegextlem1 5364  cnegextlem2 5365  cnegext 5367  addcan 5370  addcant 5371  negeu 5374  subvalt 5376  subclt 5386  subaddt 5394  negsubt 5401  subid1t 5415  mul01t 5462  mulneg1t 5470  mul2negt 5473  negdit 5474  addge0 5618  addgegt0 5619  add20 5621  mulge0 5626  ltadd1t 5642  leadd1t 5644  ltsubaddt 5646  lesubaddt 5648  lt2addt 5662  le2addt 5663  addgt0t 5666  addgegt0t 5667  addge0t 5669  lesub0t 5697  mulge0t 5698  recext 5703  mulcan 5705  mulcanOLD 5706  mulcant2 5707  mulcant2OLD 5708  mulcant 5709  mulcantOLD 5710  mul0or 5713  mul0ort 5715  receu 5720  divval 5723  divmulz 5725  divmult 5726  divclt 5731  divcan1t 5739  divcan2tOLD 5741  divrect 5753  divdirt 5764  divdirtOLD 5765  divcan3z 5768  divcan3t 5770  div11t 5773  div1t 5781  redivclt 5809  prodgt0 5828  ltmul1i 5830  prodgt0t 5835  prodge0t 5837  ltmul1t 5839  ltdiv1t 5858  ltdiv1tOLD 5859  ltmuldivt 5872  ltmuldivtOLD 5873  peano2nn 5944  nnleltp1t 5963  nnsub 5965  nnsubt 5966  nndivt 5968  halfpost 6045  nn0addclt 6129  nn0mulcl 6131  nn0mulclt 6132  nn0ltp1let 6136  nn0subt 6170  elnn0nn 6180  zltp1let 6190  nneo 6206  nneot 6207  zeot 6208  zneo 6209  dfuz 6211  uzindOLD 6217  nn0ind-raph 6223  flleltt 6237  flbit 6249  monoord 6302  om2uzsuc 6304  om2uzran 6308  seq1lem1 6317  seq1rn2 6329  shftvalt 6354  seq1shftid 6364  icoshftf1oi 6417  icoshftf1olem 6418  icoun 6421  snunioo 6423  uzind4s 6460  uzind4s2 6461  seq0fval 6543  seqzfval 6545  seqzrn2 6564  expp1t 6582  expcllem 6583  1expt 6592  expge0t 6599  expge1t 6601  mulexpt 6602  recexpt 6603  expaddt 6604  expmult 6605  expwordit 6611  expword2it 6613  exple1t 6615  sq11t 6637  sqge0t 6641  sumsqne0 6642  sq0i 6644  sqlecant 6649  sqeqort 6657  binom2t 6658  sq01t 6659  discrlem2 6665  discrlem3 6666  discrlem 6667  nn0opth2t 6676  sqrmul 6713  sqrsqt 6730  sqr2irrlem2 6733  sqr2irrlem3 6734  sqr2irrlem5 6736  crulem 6744  crut 6746  creur 6750  creui 6751  replimt 6769  readdt 6812  imaddt 6815  cjaddt 6819  cjmult 6820  cjexpt 6824  abs00 6849  absmult 6865  absdivt 6867  absexpt 6875  cjdivt 6896  abssubt 6901  abstrit 6905  abs1m 6911  recant 6912  abs3lemt 6914  facp1t 6943  faclbnd 6952  faclbnd3 6954  faclbnd4lem1 6955  faclbnd4lem2 6956  faclbnd4lem3 6957  faclbnd4lem4 6958  bcvalt 6965  bcpasc2t 6975  bcpasc 6976  bcpasct 6977  bccl2t 6978  fsump1slem 7019  fsumsplit 7027  fsumadd 7029  fsumconst 7045  serzrelem 7068  binomlem2 7074  binomlem6 7078  binom 7079  bcxmas 7083  climconst 7101  climshft 7111  iserzshft2 7114  climmulc2 7136  ser1const 7178  cvgcmp3cetlem1 7195  fnsmnt 7233  expcnvlem5 7238  expcnvlem6 7239  geoser 7241  geolim 7244  geolim1 7246  cvgratlem1ALT 7254  cvgratlem1 7257  cvgratlem4 7260  fsum0diaglem2 7264  fsum0diag 7265  fsum0diag2 7266  fsum0diag4 7268  mulc1cncf 7286  ivthlem8 7295  efcltlem2 7312  efseq1ex 7313  efvalt 7315  ef0lem 7317  efaddt 7374  efne0t 7376  efexpt 7379  eftlext 7385  ef1tlub 7389  ef01tllem1 7390  ef01tllem2 7391  ef01tllem2OLD 7392  ef01tlub 7393  absef01tlub 7395  eirr 7401  ef4pt 7407  efcnlem4 7429  sinaddt 7460  cosaddt 7461  demoivre 7492  acdc2lem1 7496  acdc5lem1 7499  infpn2 7517  ruclem4 7521  ruclem25 7542  ruclem29 7546  ruclem32 7549  retopbas 7659  meteq0 7816  mettri2 7817  mettri4 7818  blval 7841  blelrn 7852  metcni 7898  blssioo 7917  tgioolem 7918  metcnp4lem2 7973  metcnp4 7974  bcthlem15 8017  bcthlem16 8018  bcthlem17 8019  bcthlem18 8020  isgrpi 8046  grpass 8051  grpidinvlem1 8052  grpidinvlem2 8053  grpidinvlem3 8054  grpidinvlem4 8055  grpideu 8057  grpidinv2 8063  grprcan 8066  grpinveu 8067  grpinv 8072  grpinvid2 8076  isgrp2i 8079  grpdivval 8085  grplactfval 8099  ablcom 8106  issubgilem 8124  grpsn 8127  ablsn 8128  cnid 8130  mulid 8135  ghgrpilem1 8136  ghgrpilem3 8138  ghgrpilem4 8139  ghgrpi 8140  ringid 8148  ringdi 8149  ringdir 8150  ringass 8151  cnring 8165  ringsn 8166  vcdi 8174  vcdir 8175  vcass 8176  nvmul0or 8275  nvs 8293  nvtri 8301  sqcn 8338  va1cnlem 8348  sm1cnilem 8350  ipval 8356  ip1cnilem3 8378  ip1cnilem4 8379  ip1cnilem6 8381  lnolin 8418  bloval 8444  nmlno0 8458  isblo3i 8464  blo3i 8465  blocnilem 8467  phpar2 8485  phpar 8486  ipdiri 8492  ipasslem1 8493  ipasslem5 8497  ipasslem6 8498  ipasslem8 8500  ipasslem9 8501  ipasslem11 8503  ipassi 8504  siilem2 8515  sii 8517  ipblnfi 8519  ip2eqi 8520  ajfun 8524  minveclem36 8583  htthlem2 8624  sincolem 8667  sincosq1eq 8711  efifolem2 8725  efifolem3 8726  shftefif1olem 8743  hvsubvalt 8888  hvmul0ort 8896  hvsubsub4t 8929  hvsubeq0 8932  hvaddcan 8934  hvnegdit 8936  hvsubeq0t 8937  hvaddcant 8939  hvsubaddt 8946  hiidge0t 8966  his6t 8967  hial0 8970  hial02 8971  hial2eqt 8974  normlem6 8983  normlem7tALT 8987  bcseq 8988  normlem9at 8989  normgt0tOLD 8995  normgt0t 8996  normsub0t 9005  norm-iit 9007  norm-iiit 9009  normsubt 9012  normpytht 9014  norm3dift 9019  norm3lemt 9021  norm3adift 9022  normpart 9024  polidt 9028  hilid 9030  bcst 9050  shaddclt 9087  shaddcltOLD 9088  shmulclt 9089  shmulcltOLD 9090  hlimcaui 9108  ocelt 9156  occllem2 9176  occllem8 9182  projlem7 9194  projlem8 9195  projlem10 9197  projlem15 9202  projlem16 9203  projlem17 9204  projlem20 9207  pjthlem8 9228  pjthlem9 9229  pjthlem12 9232  pjth 9235  pjtheu 9237  pjeq2t 9243  omlsi 9247  pjpj0 9257  shsclt 9284  shslejt 9352  shlubt 9356  chj0t 9422  chlejb1t 9437  chnlet 9439  chjasst 9458  ledit 9465  h1de2ctlem 9480  elspansn2t 9492  spansncol 9493  spansneleq 9495  normcant 9501  pjspansnt 9502  h1datom 9506  hommvalt 9514  hfmmvalt 9517  cmbr3 9545  osumlem5 9584  osumlem8 9587  osumt 9590  spansnjt 9594  spansncvt 9600  5oalem2 9602  pjssge0 9629  pjadjt 9632  pjaddt 9633  pjsubt 9635  pjmult 9636  pjcjt2 9639  hosubclt 9701  hoaddcomt 9702  hoaddasst 9710  hocsubdirt 9713  hoaddid1t 9719  ho0subt 9725  honegsubt 9727  hosubeq0 9754  adjsymt 9761  eigre 9762  eigret 9763  eigpos 9764  eigorth 9765  eigortht 9766  specvalt 9826  lnoplt 9840  unopt 9841  hmopt 9848  lnfnlt 9857  adjt 9859  bravalvalt 9870  kbvalvalt 9880  kbpjt 9882  hoddit 9917  lnopeq0lem2 9933  lnopunilem1 9937  lnopunilem2 9938  lnopuni 9939  lnophm 9945  lnopcon 9965  lnopcnbdt 9967  lnfncon 9992  lnfncnbdt 9994  nlelch 9996  riesz4 9998  riesz1t 10000  cnlnadjlem2 10003  cnlnadjlem5 10006  cnlnadjlem8 10009  branmfnt 10040  leopg 10057  hstel2t 10149  hst1ht 10157  stjt 10165  strlem3a 10182  mdit 10225  mdbr3 10227  mdbr4 10228  dmdbrt 10229  dmdmdt 10230  dmdi4 10237  dmdbr5 10238  mdsl1 10251  cvmd 10254  mdslmd1lem3 10257  mdslmd1lem4 10258  mdslmd1 10259  superpos 10284  cvexcht 10304  atcv0eq 10309  atcv1t 10310  mdsymlem2 10334  sumdmdlem2 10349  cdjreu 10362  cdj1 10363  cdj3lem1 10364  cdj3lem2 10365  cdj3lem2b 10367  cdj3lem3b 10370  cdj3 10371  abs2sqlet 10377  abs2sqltt 10378  ghomgrpilem1 10388  ghomlin 10396  ghomf1olem 10399  elgiso 10401  cayleylem2 10413  cayleythlem 10416  hmph 10518  hmeogrp 10532  trran 10615  trnij 10616  cnvtr 10617  1ded 10650  domcmpd 10658  codcmpd 10659  cmpasso 10685  cmpidb 10687  ismonb 10717  isepib2 10729  ispgrag 10758

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-pow 2749  ax-pr 2786

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-pw 2407  df-sn 2417  df-pr 2418  df-op 2421  df-uni 2509  df-br 2626  df-opab 2673  df-xp 3191  df-cnv 3193  df-dm 3195  df-rn 3196  df-res 3197  df-ima 3198  df-fv 3205  df-opr 3972

Copyright terms: Public domain