Theorem opreq2 3969

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq2

Step	Hyp	Ref	Expression
1		opeq2 2488	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 3728	. 2 |- (A = B -> (F` <.C, A>.) = (F` <.C, B>.))
3		df-opr 3965	. 2 |- (CFA) = (F` <.C, A>.)
4		df-opr 3965	. 2 |- (CFB) = (F` <.C, B>.)
5	2, 3, 4	3eqtr4g 1531	1 |- (A = B -> (CFA) = (CFB))

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

This theorem is referenced by:  opreq12 3970  opreq2i 3972  opreq2d 3976  rcla4eopr 3990  foprcl 4015  ndmoprcl 4044  caoprcl 4052  caoprcom 4053  caoprass 4054  caoprcan 4055  caoprord 4056  caoprdistr 4059  caoprmo 4070  curry1 4098  curry1val 4100  elrnoprabg 4124  omv 4151  oev 4153  oesuc 4166  oacl 4170  omcl 4171  oecl 4172  oa0r 4173  om0r 4174  om1r 4177  oe1m 4179  oaordi 4180  oaord 4181  oawordri 4184  oawordeulem 4188  oaass 4195  oarec 4196  omordi 4197  omord2 4198  omcan 4200  omwordri 4203  om00 4206  odi 4210  omass 4211  oen0 4213  oeordi 4214  oeord 4215  oecan 4216  oewordri 4219  oeworde 4220  oelim2 4222  nnacl 4229  nnmcl 4230  nnecl 4231  nnacom 4233  nnmsucr 4240  nnmcom 4241  oaabs 4252  nneob 4255  th3qlem2 4315  th3q 4317  ecoprcom 4319  ecoprass 4320  ecoprdi 4321  map0 4344  unfilem2 4549  unfilem3 4550  addcmpblnq 5052  addclpq 5058  mulclpq 5060  recmulpq 5070  dmrecpq 5074  ltapq 5076  ltmpq 5077  ltexpq 5080  ltbtwnpq 5084  ltrpq 5085  genpv 5102  genpass 5112  distrlem1pr 5127  1idpr 5133  prlem934 5139  ltexprlem3 5144  ltexprlem4 5145  ltexpri 5149  ltaprlem 5150  ltapr 5151  prlem936 5155  reclem3pr 5158  recexpr 5160  mulcmpblnrlem 5182  addclsr 5192  mulclsr 5193  ltasr 5209  negexsr 5211  recexsrlem 5212  mulgt0sr 5214  recexsr 5216  supsrlem2 5226  addcnsr 5253  mulcnsr 5254  axaddopr 5265  axmulopr 5266  axaddrcl 5272  axmulrcl 5274  axrnegex 5283  axrrecex 5284  axcnre 5286  pre-axltadd 5289  pre-axmulgt0 5290  cnegextlem1 5345  cnegext 5348  addcan 5351  addcant 5352  negeu 5355  negeq 5359  subclt 5367  subadd 5371  subaddt 5375  negsubt 5382  ine0 5434  1re 5435  mulneg1t 5451  mul2negt 5454  negdit 5455  ltadd2 5590  addge0 5599  add20 5602  mulge0 5607  msqge0 5614  ltadd1t 5623  leadd1t 5625  ltsubaddt 5627  lesubaddt 5629  lt2addt 5643  le2addt 5644  addgt0t 5647  addgegt0t 5648  addge0t 5650  lesub0t 5678  mulge0t 5679  recextlem2 5683  recext 5684  mulcan 5686  mulcanOLD 5687  mulcant2 5688  mulcant2OLD 5689  mul0or 5694  mul0ort 5696  receu 5701  divmul 5705  divmulz 5706  divmult 5707  divclz 5711  divclt 5712  divcan1z 5718  divcan2z 5719  divcan1t 5724  divcan1tOLD 5725  divcan2tOLD 5727  recne0z 5731  recne0t 5732  recidt 5735  divrecz 5738  divrect 5739  divdirz 5749  divdirt 5750  divdirtOLD 5751  divcan3t 5760  divcan3tOLD 5761  div11t 5765  recrect 5776  rec11i 5777  rec11 5778  redivcl 5798  redivclz 5799  redivclt 5800  eqneg 5804  ltmul1 5822  ltdiv1 5824  prodgt0t 5826  prodge0t 5828  ltmul1t 5830  lemul1it 5837  lemul1itOLD 5838  ltdiv1t 5849  ltdiv1tOLD 5850  ltmuldivt 5863  ltmuldivtOLD 5864  ltrec 5879  lt2msq 5881  ltrect 5884  lerect 5885  nnaddclt 5940  nnmulclt 5941  nnsubt 5957  nndivt 5959  2timest 6004  nn0addclt 6120  nn0mulcl 6122  nn0mulclt 6123  nnnn0addclt 6125  nn0subt 6161  quoremOLD 6252  zqt 6260  qrecclt 6273  seq1rn2 6321  ser1ft 6328  shftfval 6342  icoshftf1olem 6410  icoun 6413  snunioo 6415  uzaddclt 6449  fzrevralt 6519  fzshftralt 6522  fsequb 6523  seqzfveq 6554  seqzrn2 6556  dfseq0 6563  expp1t 6574  expcllem 6575  1expt 6584  expeq0t 6585  expne0it 6588  expgt0t 6589  expge0t 6591  expgt1t 6592  expge1t 6593  mulexpt 6594  recexpt 6595  expaddt 6596  expmult 6597  expcant 6601  expwordit 6603  expmwordit 6606  exple1t 6607  sqlecant 6641  binom2t 6650  bernneq 6652  expnbndt 6654  discrlem2 6657  discrlem 6659  nn0opth2t 6668  sqrlem21 6693  sqrmul 6705  sqr2irrlem5 6728  cru 6737  crut 6738  crne0 6739  creur 6742  creui 6743  replimt 6761  reim0bt 6775  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  ser1absdiflem 6929  facdivt 6942  faclbnd3 6947  faclbnd4lem1 6948  faclbnd4lem2 6949  faclbnd4lem3 6950  faclbnd4lem4 6951  faclbnd6 6954  bcvalt 6958  bcpasc2t 6968  bcpasc 6969  bcpasct 6970  bccl2t 6971  clim 6977  fsump1slem 7012  fsumcllem 7014  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  csbfsumlem 7026  fsumcom 7028  fsumrev 7029  fsumshft 7031  fsummulc1 7033  fsumconst 7038  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  binomlem1 7066  binomlem2 7067  binomlem3 7068  binomlem4 7069  binomlem6 7071  binom 7072  bcxmaslem1 7074  bcxmas 7076  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  infcvg 7224  expcnvlem3 7229  geoser 7234  geolimilem 7235  geolim 7237  geolim1i 7238  geolim1 7239  cvgratlem1ALT 7247  cvgratlem2ALT 7248  cvgratlem1 7250  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag 7258  fsum0diag2 7259  fsum0diag4 7261  mulc1cncf 7279  ivthlem6 7286  ivthlem7 7287  efcltlem1 7304  dfef2 7307  ef0lem 7310  efclt 7312  efcvg 7314  eftval 7316  erelem2 7320  erelem3 7321  erelem6 7324  efaddlem6 7343  efaddlem24 7361  efaddlem26 7363  efaddlem27 7364  efaddt 7367  efexpt 7372  ef1tllem 7381  ef01tlub 7386  absef01tlub 7388  eirr 7394  ef4pt 7400  eflegeolem2 7414  eflegeot 7416  efm1legeot 7418  efcnlem4 7422  sinvalt 7429  cosvalt 7430  sinaddt 7453  cosaddt 7454  abseft 7483  demoivre 7484  acdc2lem1 7488  acdc5lem1 7491  infpnlem2 7507  ruclem4 7513  ruclem32 7541  infmap2 7581  retopbas 7655  meteq0 7812  mettri2 7813  mettri4 7814  elbl 7838  blelrn 7848  blss 7853  ssblex 7856  blnei 7879  metcnp 7887  blssioo 7913  tgioolem 7914  lmbr 7928  fsumcnlem 7989  bcthlem15 8013  bcthlem17 8015  isgrp 8041  grpass 8047  grpidinvlem1 8048  grpidinvlem3 8050  grpidinvlem4 8051  grpidinv 8052  grpideu 8053  grpidinv2 8060  grprcan 8063  grpinvval 8067  grpinv 8069  grpinvid1 8072  grplcan 8075  isgrp2i 8076  grplactval 8097  grplactf1o 8098  ablcom 8103  issubgilem 8121  grpsn 8124  ablsn 8125  ghgrpilem1 8133  ghgrpilem3 8135  ghgrpilem4 8136  ghgrpi 8137  ringid 8145  ringdi 8146  ringdir 8147  ringass 8148  cnring 8162  ringsn 8163  vcid 8170  vcdi 8171  vcdir 8172  vcass 8173  nvmul0or 8272  nvs 8290  nvtri 8298  sm1cnilem 8347  ipval 8353  lnolin 8415  bloval 8441  nmlno0 8455  blocnilem 8464  phpar2 8482  phpar 8483  ipdiri 8489  ipassi 8501  siilem1 8511  siii 8513  sii 8514  ip2eqi 8517  ajfun 8521  minveclem13 8557  minvecex 8578  minveceu 8583  minvecdist 8585  minveclem39 8587  htthlem2 8621  sincolem 8665  efgh 8718  efghgrpilem 8719  efif 8721  efifo 8729  efif1lem6 8735  efif1 8737  shftefif1olem 8741  eff1i 8744  effoi 8745  hvsubvalt 8886  hvmul0ort 8894  hvsubsub4t 8927  hvaddcan 8932  hvnegdit 8934  hvsubeq0t 8935  hvaddcant 8937  hvsubaddt 8944  hial0 8968  hial02 8969  hial2eqt 8972  normlem6 8981  normlem9at 8987  normsub0t 9003  norm-iit 9005  norm-iiit 9007  normsubt 9010  normpytht 9012  norm3dift 9017  norm3lemt 9019  norm3adift 9020  normpart 9022  polidt 9026  bcst 9048  hlim 9056  hlim2 9060  shaddclt 9085  shaddcltOLD 9086  shmulclt 9087  shmulcltOLD 9088  hsn0elch 9120  ocsh 9156  ocorth 9164  ocin 9169  occllem2 9174  occllem7 9179  occllem8 9180  projlem1 9186  projlem7 9192  projlem17 9202  projlem20 9205  projlem22 9207  projlem26 9211  projlem28 9213  pjthlem13 9231  pjthlem14 9232  pjtheu 9235  omlsi 9245  pjoc1 9264  shsel3t 9279  shscl 9281  shsclt 9282  choc0 9290  shslejt 9350  shlubt 9354  chlejb1t 9435  chnlet 9437  chjasst 9456  ledit 9463  h1deot 9472  h1de2 9476  elspansnt 9489  elspansn2t 9490  spanunsn 9502  h1datom 9504  pjoml6 9532  cmbr3t 9551  pjoml3t 9555  osumlem5 9582  osumlem8 9585  osumt 9588  spansncv 9597  pjadjt 9630  pjaddt 9631  pjsubt 9633  pjmult 9634  pjcjt2 9637  hosubclt 9699  hoaddcomt 9700  hoaddasst 9708  hocsubdirt 9711  ho0subt 9723  honegsubt 9725  adjsymt 9759  eigre 9760  eigret 9761  eigpos 9762  eigorth 9763  eigortht 9764  cnopct 9837  lnoplt 9838  unopt 9839  hmopt 9846  cnfnct 9854  lnfnlt 9855  adjt 9857  adjvalvalt 9861  bravalt 9867  kbvalt 9876  eleigvect 9881  hoddit 9915  lnopeq0lem2 9931  lnopuni 9937  lnophm 9943  nmcopexlem4 9954  nmcopex 9957  nmcfnexlem4 9983  nmcfnex 9986  riesz3 9995  riesz4 9996  cnlnadjlem4 10003  cnlnadjlem5 10004  cnlnadj 10009  nmopadjle 10021  nmopco 10028  cnvbravalt 10043  leopg 10055  hmopidmch 10079  pjclem3 10125  hstel2t 10146  stjt 10162  mdbrt 10221  dmdbrt 10226  mdsl0 10237  chcv1t 10282  chjatom 10284  cvexcht 10301  atcvat4 10324  sumdmdlem 10345  cdjreu 10359  cdj1 10360  cdj3lem1 10361  cdj3lem2 10362  cdj3lem2b 10364  cdj3lem3b 10367  cdj3 10368  ghomgrpilem1 10385  ghomlin 10393  elgiso 10398  cayleylem2 10410  cayleythlem 10413  hmph 10524  iintlem1 10632  iintlem2 10633  1ded 10671  domcmpd 10679  codcmpd 10680  cmpasso 10706  cmpida 10707  ismonb2 10740  cmpmon 10743  icmpmon 10744  idmon 10745  isepib 10748

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