Theorem opreq1 3006

Description: Equality theorem for operations.

Assertion

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

Proof of Theorem opreq1

Step	Hyp	Ref	Expression
1		opeq1 1876	. . 3 |- (A = B -> <.A, C>. = <.B, C>.)
2	1	fveq2d 2836	. 2 |- (A = B -> (F` <.A, C>.) = (F` <.B, C>.))
3		df-opr 3003	. 2 |- (AFC) = (F` <.A, C>.)
4		df-opr 3003	. 2 |- (BFC) = (F` <.B, C>.)
5	2, 3, 4	3eqtr4g 1147	1 |- (A = B -> (AFC) = (BFC))

Syntax hints:   -> wi 2   = wceq 1091  <.cop 1810  ` cfv 2422  (class class class)co 3001

This theorem is referenced by:  opreq12 3008  opreq1i 3009  opreq1d 3012  caoprcl 3066  caoprcom 3067  caoprass 3068  caoprcan 3069  caoprord 3070  caoprdistr 3073  caoprmo 3084  oe0 3130  omsuc 3133  oesuc 3134  oecl 3140  om0r 3142  om1r 3145  oe1m 3147  oawordeu 3157  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmcom 3183  nnmord 3189  th3qlem2 3251  th3q 3253  ecoprcom 3255  ecoprass 3256  ecoprdi 3257  map0 3268  mapdom2 3389  unfilem3 3440  addcmpblnq 3846  addclpq 3852  mulclpq 3854  mulidpq 3863  recmulpq 3864  ltapq 3870  ltmpq 3871  ltexpq 3874  genpv 3896  genpass 3906  distrlem4pr 3924  prlem934a 3931  prlem934b 3932  ltexprlem7 3942  prlem936 3949  mulcmpblnrlem 3976  addclsr 3986  mulclsr 3987  0idsr 4000  1idsr 4001  00sr 4002  ltasr 4003  recexsrlem 4006  mulgt0sr 4008  suppsr 4016  suppsr2 4017  supsrlem4 4022  supsr 4025  addcnsr 4047  mulcnsr 4048  axaddcl 4066  axaddrcl 4067  axmulcl 4068  axmulrcl 4069  ax0id 4076  ax1id 4077  axnegex 4078  axrecex 4079  axrnegex 4080  axrrecex 4081  axltadd 4085  axmulgt0 4086  axcnre 4087  addcan 4120  addcant 4122  negeu 4124  subval 4134  subclt 4140  subaddt 4145  subnegt 4149  subid1t 4160  subeq0 4163  subeq0t 4169  subdit 4184  mulzer1t 4188  mulneg1t 4196  mul2negt 4199  negdit 4200  mulcan 4207  mulcant 4208  mulcant2 4209  mul0or 4210  mul0ort 4212  receu 4215  divval 4217  divmulz 4219  divmult 4220  divclt 4223  divcan1t 4228  divcan2t 4229  divrect 4238  divdistrt 4246  divcan3z 4249  divcan3t 4251  div1t 4258  redivclt 4276  addge0 4324  addgegt0 4325  add20 4329  mulge0 4335  ltadd1t 4348  leadd1t 4350  ltsubaddt 4353  lesubaddt 4355  lt2addt 4361  addge0t 4362  posdift 4365  lesub0t 4374  mulge0t 4375  prodgt0 4388  divge0 4392  divgt0t 4402  divge0t 4403  ltdivt 4404  ltmuldivt 4406  ltdiv23t 4419  peano2nn 4433  nnleltp1t 4448  nnsub 4450  nnsubt 4451  nndiv 4453  halfpost 4508  crulem 4528  cru 4529  crut 4531  creur 4532  creui 4533  nn0addclt 4551  nn0mulcl 4553  nn0mulclt 4554  nn0ltp1let 4556  nn0subt 4587  elnn0nn 4593  zltp1let 4597  zneo 4601  uzind 4603  nn0ind 4612  flleltt 4625  znq 4630  qaddclt 4642  qnegclt 4643  qmulclt 4644  qrecclt 4646  om2uzsuc 4652  om2uzran 4655  seqlem1 4662  seqrn 4673  0expt 4680  1expt 4681  expcllem 4682  expaddt 4698  sqe11t 4705  lt2sqet 4706  sqege0t 4708  discrlem2 4714  discrlem3 4715  discrlem 4716  nneo 4719  nn0opth2t 4726  sqrmul 4763  sqr2irrlem2 4778  sqr2irrlem3 4779  sqr2irrlem5 4781  replimt 4798  reim0 4809  rere 4810  cjaddt 4831  cjmult 4832  abs00 4839  absmult 4849  abssubt 4864  abs3lemt 4865  facp1t 4873  ruclem4 4888  ruclem25 4909  ruclem29 4913  ruclem32 4916  hvsubvalt 4997  hvsubsub4t 5032  hvsubeq0 5035  hvaddcan 5037  hvnegdit 5039  hvsubeq0t 5040  hvsubaddt 5042  hiidge0t 5056  his6 5057  hial0 5058  hial2eqt 5060  normlem6 5068  normlem7t 5072  bcseq 5073  normgt0t 5078  normsub0t 5085  norm-iiit 5088  normsubt 5091  normpytht 5092  norm3lemt 5097  norm3adift 5098  shaddclt 5123  shmulclt 5124  hlimcaui 5141  ocelt 5162  occllem2 5181  occllem8 5187  projlem7 5199  projlem8 5200  projlem10 5202  projlem15 5207  projlem16 5208  projlem17 5209  projlem20 5212  pjthlem8 5232  pjthlem9 5233  pjthlem12 5236  pjthlem14 5238  pjth 5239  pjthu 5241  pjthu2 5242  omlsi 5250  pjpj0 5259  pjpjtht 5262  shscl 5282  shsclt 5283  shsvat 5285  shunss 5338  shslejt 5351  shlubt 5355  chj0t 5414  chlejb1t 5429  chnlet 5431  chjasst 5446  h1de2ctlem 5460  elspansn2t 5472  spansncol 5473  spansneleq 5475  spanunsn 5482  h1datom 5483  cmbr3 5509  osumlem5 5534  osumlem8 5537  spansnjt 5540  spansncvt 5543  5oalem2 5545  pjssge0 5573  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  pjjs 5585  stjt 5676  strlem3a 5693  mdi 5727  mdbr3 5729  mdbr4 5730  dmdbr 5731  cvexcht 5763  atcv0eq 5767  atcv1 5768  mdsymlem2 5777

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438  df-opr 3003

metamath.org