Theorem opreq1 3968

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq1

Step	Hyp	Ref	Expression
1		opeq1 2487	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	fveq2d 3728	. 2 |- (A = B -> (F` <.A, C>.) = (F` <.B, C>.))
3		df-opr 3965	. 2 |- (AFC) = (F` <.A, C>.)
4		df-opr 3965	. 2 |- (BFC) = (F` <.B, C>.)
5	2, 3, 4	3eqtr4g 1531	1 |- (A = B -> (AFC) = (BFC))

Syntax hints:   -> wi 3   = wceq 956  <.cop 2411  ` cfv 3182  (class class class)co 3963

This theorem is referenced by:  opreq12 3970  opreq1i 3971  opreq1d 3975  rcla4eopr 3990  foprcl 4015  caoprcl 4052  caoprcom 4053  caoprass 4054  caoprcan 4055  caoprord 4056  caoprdistr 4059  caoprmo 4070  elrnoprabg 4124  oe0 4161  oev2 4162  omsuc 4165  oesuc 4166  oecl 4172  om0r 4174  om1r 4177  oe1m 4179  oawordeu 4189  omord 4199  omwordi 4202  om00 4206  odi 4210  omass 4211  oewordi 4218  oewordri 4219  oelim2 4222  nnacom 4233  nnmsucr 4240  nnmcom 4241  nneob 4255  th3qlem2 4315  th3q 4317  ecoprcom 4319  ecoprass 4320  ecoprdi 4321  map0 4344  mapdom2 4494  unfilem3 4550  addcmpblnq 5052  addclpq 5058  mulclpq 5060  mulidpq 5069  recmulpq 5070  ltapq 5076  ltmpq 5077  ltexpq 5080  genpv 5102  genpass 5112  distrlem4pr 5130  prlem934a 5137  prlem934b 5138  ltexprlem7 5148  prlem936 5155  mulcmpblnrlem 5182  addclsr 5192  mulclsr 5193  0idsr 5206  1idsr 5207  00sr 5208  ltasr 5209  recexsrlem 5212  mulgt0sr 5214  suppsr 5222  suppsr2 5223  supsrlem4 5228  supsr 5231  addcnsr 5253  mulcnsr 5254  axaddopr 5265  axmulopr 5266  axaddrcl 5272  axmulrcl 5274  ax0id 5281  ax1id 5282  axrnegex 5283  axrrecex 5284  axcnre 5286  pre-axltadd 5289  pre-axmulgt0 5290  cnegextlem1 5345  cnegextlem2 5346  cnegext 5348  addcan 5351  addcant 5352  negeu 5355  subvalt 5357  subclt 5367  subaddt 5375  negsubt 5382  subid1t 5396  mul01t 5443  mulneg1t 5451  mul2negt 5454  negdit 5455  addge0 5599  addgegt0 5600  add20 5602  mulge0 5607  ltadd1t 5623  leadd1t 5625  ltsubaddt 5627  lesubaddt 5629  lt2addt 5643  le2addt 5644  addgt0t 5647  addgegt0t 5648  addge0t 5650  lesub0t 5678  mulge0t 5679  recext 5684  mulcan 5686  mulcanOLD 5687  mulcant2 5688  mulcant2OLD 5689  mulcant 5690  mulcantOLD 5691  mul0or 5694  mul0ort 5696  receu 5701  divval 5704  divmulz 5706  divmult 5707  divclt 5712  divcan1t 5724  divcan1tOLD 5725  divcan2tOLD 5727  divrect 5739  divdirt 5750  divdirtOLD 5751  divcan3z 5754  divcan3t 5760  divcan3tOLD 5761  div11t 5765  div1t 5773  redivclt 5800  prodgt0 5819  ltmul1i 5821  prodgt0t 5826  prodge0t 5828  ltmul1t 5830  ltdiv1t 5849  ltdiv1tOLD 5850  ltmuldivt 5863  ltmuldivtOLD 5864  peano2nn 5935  nnleltp1t 5954  nnsub 5956  nnsubt 5957  nndivt 5959  halfpost 6036  nn0addclt 6120  nn0mulcl 6122  nn0mulclt 6123  nn0ltp1let 6127  nn0subt 6161  elnn0nn 6171  zltp1let 6181  nneo 6197  nneot 6198  zeot 6199  zneo 6200  dfuz 6202  uzindOLD 6208  nn0ind-raph 6214  flleltt 6228  flbit 6240  monoord 6294  om2uzsuc 6296  om2uzran 6300  seq1lem1 6309  seq1rn2 6321  shftvalt 6346  seq1shftid 6356  icoshftf1oi 6409  icoshftf1olem 6410  icoun 6413  snunioo 6415  uzind4s 6452  uzind4s2 6453  seq0fval 6535  seqzfval 6537  seqzrn2 6556  expp1t 6574  expcllem 6575  1expt 6584  expge0t 6591  expge1t 6593  mulexpt 6594  recexpt 6595  expaddt 6596  expmult 6597  expwordit 6603  expword2it 6605  exple1t 6607  sq11t 6629  sqge0t 6633  sumsqne0 6634  sq0i 6636  sqlecant 6641  sqeqort 6649  binom2t 6650  sq01t 6651  discrlem2 6657  discrlem3 6658  discrlem 6659  nn0opth2t 6668  sqrmul 6705  sqrsqt 6722  sqr2irrlem2 6725  sqr2irrlem3 6726  sqr2irrlem5 6728  crulem 6736  crut 6738  creur 6742  creui 6743  replimt 6761  readdt 6805  imaddt 6808  cjaddt 6812  cjmult 6813  cjexpt 6817  abs00 6842  absmult 6858  absdivt 6860  absexpt 6868  cjdivt 6889  abssubt 6894  abstrit 6898  abs1m 6904  recant 6905  abs3lemt 6907  facp1t 6936  faclbnd 6945  faclbnd3 6947  faclbnd4lem1 6948  faclbnd4lem2 6949  faclbnd4lem3 6950  faclbnd4lem4 6951  bcvalt 6958  bcpasc2t 6968  bcpasc 6969  bcpasct 6970  bccl2t 6971  fsump1slem 7012  fsumsplit 7020  fsumadd 7022  fsumconst 7038  serzrelem 7061  binomlem2 7067  binomlem6 7071  binom 7072  bcxmas 7076  climconst 7094  climshft 7104  iserzshft2 7107  climmulc2 7129  ser1const 7171  cvgcmp3cetlem1 7188  fnsmnt 7226  expcnvlem5 7231  expcnvlem6 7232  geoser 7234  geolim 7237  geolim1 7239  cvgratlem1ALT 7247  cvgratlem1 7250  cvgratlem4 7253  fsum0diaglem2 7257  fsum0diag 7258  fsum0diag2 7259  fsum0diag4 7261  mulc1cncf 7279  ivthlem8 7288  efcltlem2 7305  efseq1ex 7306  efvalt 7308  ef0lem 7310  efaddt 7367  efne0t 7369  efexpt 7372  eftlext 7378  ef1tlub 7382  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  ef01tlub 7386  absef01tlub 7388  eirr 7394  ef4pt 7400  efcnlem4 7422  sinaddt 7453  cosaddt 7454  demoivre 7484  acdc2lem1 7488  acdc5lem1 7491  infpn2 7509  ruclem4 7513  ruclem25 7534  ruclem29 7538  ruclem32 7541  retopbas 7655  meteq0 7812  mettri2 7813  mettri4 7814  blval 7837  blelrn 7848  metcni 7894  blssioo 7913  tgioolem 7914  metcnp4lem2 7969  metcnp4 7970  bcthlem15 8013  bcthlem16 8014  bcthlem17 8015  bcthlem18 8016  isgrpi 8042  grpass 8047  grpidinvlem1 8048  grpidinvlem2 8049  grpidinvlem3 8050  grpidinvlem4 8051  grpideu 8053  grpidinv2 8060  grprcan 8063  grpinveu 8064  grpinv 8069  grpinvid2 8073  isgrp2i 8076  grpdivval 8082  grplactfval 8096  ablcom 8103  issubgilem 8121  grpsn 8124  ablsn 8125  cnid 8127  mulid 8132  ghgrpilem1 8133  ghgrpilem3 8135  ghgrpilem4 8136  ghgrpi 8137  ringid 8145  ringdi 8146  ringdir 8147  ringass 8148  cnring 8162  ringsn 8163  vcdi 8171  vcdir 8172  vcass 8173  nvmul0or 8272  nvs 8290  nvtri 8298  sqcn 8335  va1cnlem 8345  sm1cnilem 8347  ipval 8353  ip1cnilem3 8375  ip1cnilem4 8376  ip1cnilem6 8378  lnolin 8415  bloval 8441  nmlno0 8455  isblo3i 8461  blo3i 8462  blocnilem 8464  phpar2 8482  phpar 8483  ipdiri 8489  ipasslem1 8490  ipasslem5 8494  ipasslem6 8495  ipasslem8 8497  ipasslem9 8498  ipasslem11 8500  ipassi 8501  siilem2 8512  sii 8514  ipblnfi 8516  ip2eqi 8517  ajfun 8521  minveclem36 8580  htthlem2 8621  sincolem 8665  sincosq1eq 8709  efifolem2 8723  efifolem3 8724  shftefif1olem 8741  hvsubvalt 8886  hvmul0ort 8894  hvsubsub4t 8927  hvsubeq0 8930  hvaddcan 8932  hvnegdit 8934  hvsubeq0t 8935  hvaddcant 8937  hvsubaddt 8944  hiidge0t 8964  his6t 8965  hial0 8968  hial02 8969  hial2eqt 8972  normlem6 8981  normlem7tALT 8985  bcseq 8986  normlem9at 8987  normgt0tOLD 8993  normgt0t 8994  normsub0t 9003  norm-iit 9005  norm-iiit 9007  normsubt 9010  normpytht 9012  norm3dift 9017  norm3lemt 9019  norm3adift 9020  normpart 9022  polidt 9026  hilid 9028  bcst 9048  shaddclt 9085  shaddcltOLD 9086  shmulclt 9087  shmulcltOLD 9088  hlimcaui 9106  ocelt 9154  occllem2 9174  occllem8 9180  projlem7 9192  projlem8 9193  projlem10 9195  projlem15 9200  projlem16 9201  projlem17 9202  projlem20 9205  pjthlem8 9226  pjthlem9 9227  pjthlem12 9230  pjth 9233  pjtheu 9235  pjeq2t 9241  omlsi 9245  pjpj0 9255  shsclt 9282  shslejt 9350  shlubt 9354  chj0t 9420  chlejb1t 9435  chnlet 9437  chjasst 9456  ledit 9463  h1de2ctlem 9478  elspansn2t 9490  spansncol 9491  spansneleq 9493  normcant 9499  pjspansnt 9500  h1datom 9504  hommvalt 9512  hfmmvalt 9515  cmbr3 9543  osumlem5 9582  osumlem8 9585  osumt 9588  spansnjt 9592  spansncvt 9598  5oalem2 9600  pjssge0 9627  pjadjt 9630  pjaddt 9631  pjsubt 9633  pjmult 9634  pjcjt2 9637  hosubclt 9699  hoaddcomt 9700  hoaddasst 9708  hocsubdirt 9711  hoaddid1t 9717  ho0subt 9723  honegsubt 9725  hosubeq0 9752  adjsymt 9759  eigre 9760  eigret 9761  eigpos 9762  eigorth 9763  eigortht 9764  specvalt 9824  lnoplt 9838  unopt 9839  hmopt 9846  lnfnlt 9855  adjt 9857  bravalvalt 9868  kbvalvalt 9878  kbpjt 9880  hoddit 9915  lnopeq0lem2 9931  lnopunilem1 9935  lnopunilem2 9936  lnopuni 9937  lnophm 9943  lnopcon 9963  lnopcnbdt 9965  lnfncon 9990  lnfncnbdt 9992  nlelch 9994  riesz4 9996  riesz1t 9998  cnlnadjlem2 10001  cnlnadjlem5 10004  cnlnadjlem8 10007  branmfnt 10038  leopg 10055  hstel2t 10146  hst1ht 10154  stjt 10162  strlem3a 10179  mdit 10222  mdbr3 10224  mdbr4 10225  dmdbrt 10226  dmdmdt 10227  dmdi4 10234  dmdbr5 10235  mdsl1 10248  cvmd 10251  mdslmd1lem3 10254  mdslmd1lem4 10255  mdslmd1 10256  superpos 10281  cvexcht 10301  atcv0eq 10306  atcv1t 10307  mdsymlem2 10331  sumdmdlem2 10346  cdjreu 10359  cdj1 10360  cdj3lem1 10361  cdj3lem2 10362  cdj3lem2b 10364  cdj3lem3b 10367  cdj3 10368  abs2sqlet 10374  abs2sqltt 10375  ghomgrpilem1 10385  ghomlin 10393  ghomf1olem 10396  elgiso 10398  cayleylem2 10410  cayleythlem 10413  hmph 10524  hmeogrp 10538  trran 10636  trnij 10637  cnvtr 10638  1ded 10671  domcmpd 10679  codcmpd 10680  cmpasso 10706  cmpidb 10708  ismonb 10738  isepib2 10750  ispgrag 10779

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-xp 3184  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198  df-opr 3965

Copyright terms: Public domain