Theorem opreq2 3007

Description: Equality theorem for operations.

Assertion

Ref	Expression
opreq2	|- (A = B -> (CFA) = (CFB))

Proof of Theorem opreq2

Step	Hyp	Ref	Expression
1		opeq2 1877	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 2836	. 2 |- (A = B -> (F` <.C, A>.) = (F` <.C, B>.))
3		df-opr 3003	. 2 |- (CFA) = (F` <.C, A>.)
4		df-opr 3003	. 2 |- (CFB) = (F` <.C, B>.)
5	2, 3, 4	3eqtr4g 1147	1 |- (A = B -> (CFA) = (CFB))

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

This theorem is referenced by:  opreq12 3008  opreq2i 3010  opreq2d 3013  ndmoprcl 3058  caoprcl 3066  caoprcom 3067  caoprass 3068  caoprcan 3069  caoprord 3070  caoprdistr 3073  caoprmo 3084  omv 3120  oev 3122  oesuc 3134  oacl 3138  omcl 3139  oecl 3140  oa0r 3141  om0r 3142  om1r 3145  oe1m 3147  oaordi 3148  oaord 3149  oawordri 3152  oawordeulem 3156  oaass 3163  omordi 3164  oen0 3165  nnacl 3172  nnmcl 3173  nnacom 3175  nndi 3180  nnmass 3181  nnmsucr 3182  nnmcom 3183  nnmordi 3188  nnmord 3189  nnmcan 3190  th3qlem2 3251  th3q 3253  ecoprcom 3255  ecoprass 3256  ecoprdi 3257  map0 3268  unfilem2 3439  unfilem3 3440  addcmpblnq 3846  addclpq 3852  mulclpq 3854  recmulpq 3864  dmrecpq 3868  ltapq 3870  ltmpq 3871  ltexpq 3874  ltbtwnpq 3878  ltrpq 3879  genpv 3896  genpass 3906  distrlem1pr 3921  1idpr 3927  prlem934 3933  ltexprlem3 3938  ltexprlem4 3939  ltexpri 3943  ltaprlem 3944  ltapr 3945  prlem936 3949  reclem3pr 3952  recexpr 3954  mulcmpblnrlem 3976  addclsr 3986  mulclsr 3987  ltasr 4003  negexsr 4005  recexsrlem 4006  mulgt0sr 4008  recexsr 4010  supsrlem2 4020  addcnsr 4047  mulcnsr 4048  axaddcl 4066  axaddrcl 4067  axmulcl 4068  axmulrcl 4069  axnegex 4078  axrecex 4079  axrnegex 4080  axrrecex 4081  axltadd 4085  axmulgt0 4086  addcan 4120  addcant 4122  negeu 4124  negeq 4136  subclt 4140  subadd 4143  subaddt 4145  subnegt 4149  subeq0t 4169  subdit 4184  mulneg1t 4196  mul2negt 4199  negdit 4200  mulcan 4207  mulcant 4208  mul0or 4210  mul0ort 4212  receu 4215  divmul 4218  divmulz 4219  divmult 4220  divclz 4222  divclt 4223  divcan1z 4226  divcan2z 4227  divcan1t 4228  divcan2t 4229  recneq0z 4232  recidt 4235  divrecz 4237  divrect 4238  divdistrz 4245  divdistrt 4246  divcan3t 4251  recrect 4260  rec11i 4261  rec11 4262  redivcl 4274  redivclz 4275  redivclt 4276  addge0 4324  add20 4329  mulge0 4335  sqge0 4344  ltadd1t 4348  leadd1t 4350  ltsubaddt 4353  lesubaddt 4355  lt2addt 4361  addge0t 4362  posdift 4365  lesub0t 4374  mulge0t 4375  eqneg 4378  recgt0 4386  divgt0 4390  divge0 4392  ltmul1 4394  ltdiv 4399  recgt0t 4401  divgt0t 4402  divge0t 4403  ltdivt 4404  ltmuldivt 4406  ltrec 4410  ltdiv23 4413  lt2sq 4414  ltrect 4417  lerect 4418  ltdiv23t 4419  nnaddclt 4436  nnmulclt 4437  nnsubt 4451  nndiv 4453  2timest 4490  ine0 4524  nn0addclt 4551  nn0mulcl 4553  nn0mulclt 4554  nn0subt 4587  znq 4630  zqt 4632  qaddclt 4642  qnegclt 4643  qmulclt 4644  qrecclt 4646  seqrn 4673  0expt 4680  1expt 4681  expcllem 4682  expaddt 4698  discrlem2 4714  discrlem 4716  nn0opth2t 4726  sqrlem21 4751  sqrmul 4763  sqr2irrlem5 4781  cjaddt 4831  cjmult 4832  absmult 4849  abssubt 4864  abs3lemt 4865  clim 4877  clim2 4881  ruclem4 4888  ruclem32 4916  infmap2 4953  hvsubvalt 4997  hvsubsub4t 5032  hvaddcan 5037  hvnegdit 5039  hvsubeq0t 5040  hvsubaddt 5042  hial0 5058  hial2eqt 5060  normlem6 5068  normsub0t 5085  norm-iiit 5088  normsubt 5091  normpytht 5092  norm3lemt 5097  norm3adift 5098  hlim 5108  hlim2 5112  shaddclt 5123  shmulclt 5124  hsn0elch 5155  ocsh 5164  ocorth 5172  ocin 5177  occllem2 5181  occllem7 5186  occllem8 5187  projlem1 5193  projlem7 5199  projlem17 5209  projlem20 5212  projlem22 5214  projlem26 5218  projlem28 5220  pjthlem13 5237  pjthlem14 5238  pjthu 5241  pjthu2 5242  omlsi 5250  pjpjtht 5262  pjoc1 5268  shscl 5282  shsclt 5283  shsvat 5285  choc0 5291  shunss 5338  shslejt 5351  shlubt 5355  chlejb1t 5429  chnlet 5431  chjasst 5446  h1deot 5454  h1de2 5458  elspansnt 5471  elspansn2t 5472  spanunsn 5482  h1datom 5483  pjoml5 5498  pjoml3t 5517  osumlem5 5534  osumlem8 5537  spansncv 5542  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  pjjs 5585  pjclem3 5651  stjt 5676  mdbr 5726  chcv1t 5751  cvexcht 5763  atcvat4 5775  sumdmdlem 5786

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