Theorem opreq2 3954

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq2

Step	Hyp	Ref	Expression
1		opeq2 2479	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 3713	. 2 |- (A = B -> (F` <.C, A>.) = (F` <.C, B>.))
3		df-opr 3950	. 2 |- (CFA) = (F` <.C, A>.)
4		df-opr 3950	. 2 |- (CFB) = (F` <.C, B>.)
5	2, 3, 4	3eqtr4g 1523	1 |- (A = B -> (CFA) = (CFB))

Syntax hints:   -> wi 3   = wceq 953  <.cop 2401  ` cfv 3172  (class class class)co 3948

This theorem is referenced by:  opreq12 3955  opreq2i 3957  opreq2d 3961  rcla4eopr 3975  foprcl 4000  ndmoprcl 4030  caoprcl 4038  caoprcom 4039  caoprass 4040  caoprcan 4041  caoprord 4042  caoprdistr 4045  caoprmo 4056  curry1 4082  curry1val 4084  elrnoprabg 4108  omv 4135  oev 4137  oesuc 4150  oacl 4154  omcl 4155  oecl 4156  oa0r 4157  om0r 4158  om1r 4161  oe1m 4163  oaordi 4164  oaord 4165  oawordri 4168  oawordeulem 4172  oaass 4179  oarec 4180  omordi 4181  omord2 4182  omcan 4184  omwordri 4187  om00 4190  odi 4194  omass 4195  oen0 4197  oeordi 4198  oeord 4199  oecan 4200  oewordri 4203  oeworde 4204  oelim2 4206  nnacl 4213  nnmcl 4214  nnecl 4215  nnacom 4217  nnmsucr 4224  nnmcom 4225  oaabs 4236  nneob 4239  th3qlem2 4299  th3q 4301  ecoprcom 4303  ecoprass 4304  ecoprdi 4305  map0 4328  unfilem2 4525  unfilem3 4526  addcmpblnq 5024  addclpq 5030  mulclpq 5032  recmulpq 5042  dmrecpq 5046  ltapq 5048  ltmpq 5049  ltexpq 5052  ltbtwnpq 5056  ltrpq 5057  genpv 5074  genpass 5084  distrlem1pr 5099  1idpr 5105  prlem934 5111  ltexprlem3 5116  ltexprlem4 5117  ltexpri 5121  ltaprlem 5122  ltapr 5123  prlem936 5127  reclem3pr 5130  recexpr 5132  mulcmpblnrlem 5154  addclsr 5164  mulclsr 5165  ltasr 5181  negexsr 5183  recexsrlem 5184  mulgt0sr 5186  recexsr 5188  supsrlem2 5198  addcnsr 5225  mulcnsr 5226  axaddopr 5237  axmulopr 5238  axaddrcl 5244  axmulrcl 5246  axrnegex 5255  axrrecex 5256  axcnre 5258  pre-axltadd 5261  pre-axmulgt0 5262  cnegextlem1 5317  cnegext 5320  addcan 5323  addcant 5324  negeu 5327  negeq 5331  subclt 5339  subadd 5343  subaddt 5347  negsubt 5354  ine0 5406  1re 5407  mulneg1t 5423  mul2negt 5426  negdit 5427  ltadd2 5564  addge0 5573  add20 5576  mulge0 5581  msqge0 5588  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  lesubaddt 5603  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  lesub0t 5651  mulge0t 5652  recextlem2 5656  recext 5657  mulcan 5659  mulcant2 5660  mul0or 5663  mul0ort 5665  receu 5670  divmul 5674  divmulz 5675  divmult 5676  divclz 5680  divclt 5681  divcan1z 5687  divcan2z 5688  divcan1t 5689  divcan2t 5690  recne0z 5694  recne0t 5695  recidt 5698  divrecz 5701  divrect 5702  divdirz 5712  divdirt 5713  divcan3t 5718  div11t 5721  recrect 5732  rec11i 5733  rec11 5734  redivcl 5754  redivclz 5755  redivclt 5756  eqneg 5760  ltmul1 5778  ltdiv1 5780  prodgt0t 5782  prodge0t 5784  ltmul1t 5786  lemul1it 5793  lemul1itOLD 5794  ltdiv1t 5805  ltmuldivt 5817  ltrec 5827  lt2msq 5829  ltrect 5832  lerect 5833  nnaddclt 5888  nnmulclt 5889  nnsubt 5904  nndivt 5906  2timest 5951  nn0addclt 6067  nn0mulcl 6069  nn0mulclt 6070  nnnn0addclt 6072  nn0subt 6108  zqt 6198  qrecclt 6211  seq1rn2 6258  ser1ft 6265  shftfval 6279  icoshftf1olem 6343  icoun 6346  snunioo 6348  uzaddclt 6381  fzrevralt 6451  fzshftralt 6454  fsequb 6455  seqzfveq 6486  seqzrn2 6488  dfseq0 6495  expp1t 6506  expcllem 6507  1expt 6516  expeq0t 6517  expne0it 6519  expgt0t 6520  expge0t 6522  expgt1t 6523  expge1t 6524  mulexpt 6525  recexpt 6526  expaddt 6527  expmult 6528  expcant 6532  expwordit 6534  expmwordit 6537  exple1t 6538  sqlecant 6572  binom2t 6581  bernneq 6583  expnbndt 6585  discrlem2 6587  discrlem 6589  nn0opth2t 6598  sqrlem21 6623  sqrmul 6635  sqr2irrlem5 6658  cru 6667  crut 6668  crne0 6670  creur 6673  creui 6674  replimt 6692  readdt 6740  imaddt 6743  cjaddt 6747  cjmult 6748  cjexpt 6752  absmult 6793  absdivt 6795  absexpt 6803  cjdivt 6827  abssubt 6832  abstrit 6835  abs1m 6841  recant 6842  abs3lemt 6844  ser1absdiflem 6866  facdivt 6879  faclbnd3 6884  faclbnd4lem1 6885  faclbnd4lem2 6886  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd6 6891  bcvalt 6895  bcpasc2t 6906  bcpasc 6907  bcpasct 6908  bccl2t 6909  clim 6915  fsump1slem 6950  fsumcllem 6952  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  csbfsumlem 6964  fsumcom 6966  fsumrev 6967  fsumshft 6969  fsummulc1 6971  fsumconst 6976  fsumcmp 6978  fsumcmpndx2 6980  fsumabs 6981  binomlem1 7004  binomlem2 7005  binomlem3 7006  binomlem4 7007  binomlem6 7009  binom 7010  bcxmaslem1 7012  bcxmas 7014  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  infcvg 7159  expcnvlem3 7164  geoser 7169  geolimilem 7170  geolim 7172  geolim1i 7173  geolim1 7174  cvgratlem1ALT 7182  cvgratlem2ALT 7183  cvgratlem1 7185  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag 7193  fsum0diag2 7194  fsum0diag4 7196  mulc1cncf 7214  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  efcltlem1 7246  dfef2 7249  ef0lem 7252  efclt 7254  efcvg 7256  eftval 7258  erelem2 7262  erelem3 7263  erelem6 7266  efaddlem6 7285  efaddlem24 7303  efaddlem26 7305  efaddlem27 7306  efaddt 7309  efexpt 7314  ef1tllem 7323  ef01tlub 7327  absef01tlub 7329  eirr 7335  ef4pt 7341  eflegeolem2 7354  eflegeot 7356  efm1legeot 7358  efcnlem4 7362  sinvalt 7371  cosvalt 7372  sinaddt 7395  cosaddt 7396  abseft 7425  demoivre 7426  acdc2lem1 7430  acdc5lem1 7433  infpnlem2 7450  ruclem4 7456  ruclem32 7484  infmap2 7523  retopbas 7597  meteq0 7751  mettri2 7752  mettri4 7753  elbl 7778  blelrn 7788  blss 7793  ssblex 7796  blnei 7818  metcnp 7826  blssioo 7852  tgioolem 7853  lmbr 7866  fsumcnlem 7923  bcthlem15 7947  bcthlem17 7949  isgrp 7975  grpass 7981  grpidinvlem1 7982  grpidinvlem3 7984  grpidinvlem4 7985  grpidinv 7986  grpideu 7987  grpidinv2 7994  grprcan 7997  grpinvval 8001  grpinv 8003  grpinvid1 8006  grplcan 8010  isgrp2i 8011  grplactval 8033  grplactf1o 8034  ablcom 8039  issubgilem 8058  grpsn 8061  ablsn 8062  ghgrpilem1 8070  ghgrpilem3 8072  ghgrpilem4 8073  ghgrpi 8074  ringid 8082  ringdi 8083  ringdir 8084  ringass 8085  cnring 8099  ringsn 8100  vcid 8107  vcdi 8108  vcdir 8109  vcass 8110  nvmul0or 8212  nvs 8229  nvtri 8237  sm1cnilem 8281  ipval 8287  lnolin 8349  bloval 8373  nmlno0 8387  blocnilem 8395  phpar2 8413  phpar 8414  ipdiri 8420  ipassi 8432  siilem1 8442  siii 8444  sii 8445  ip2eqi 8448  ajfun 8452  minveclem13 8488  minvecex 8509  minveceu 8514  minvecdist 8516  minveclem39 8518  htthlem2 8551  sincolem 8584  efgh 8633  efghgrpilem 8634  efif 8636  efifo 8644  efif1lem6 8650  efif1 8652  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  effoi 8666  effoiOLD 8667  hvsubvalt 8807  hvmul0ort 8815  hvsubsub4t 8848  hvaddcan 8853  hvnegdit 8855  hvsubeq0t 8856  hvaddcant 8858  hvsubaddt 8865  hial0 8889  hial02 8890  hial2eqt 8893  normlem6 8902  normlem9at 8908  normsub0t 8924  norm-iit 8926  norm-iiit 8928  normsubt 8931  normpytht 8933  norm3dift 8938  norm3lemt 8940  norm3adift 8941  normpart 8943  polidt 8947  bcst 8969  hlim 8977  hlim2 8981  shaddclt 9006  shaddcltOLD 9007  shmulclt 9008  shmulcltOLD 9009  hsn0elch 9041  ocsh 9072  ocorth 9080  ocin 9085  occllem2 9090  occllem7 9095  occllem8 9096  projlem1 9102  projlem7 9108  projlem17 9118  projlem20 9121  projlem22 9123  projlem26 9127  projlem28 9129  pjthlem13 9146  pjthlem14 9147  pjtheu 9150  omlsi 9160  pjoc1 9179  shsel3t 9194  shscl 9196  shsclt 9197  choc0 9205  shslejt 9265  shlubt 9269  chlejb1t 9350  chnlet 9352  chjasst 9371  ledit 9378  h1deot 9387  h1de2 9391  elspansnt 9405  elspansn2t 9406  spanunsn 9419  h1datom 9421  pjoml6 9449  cmbr3t 9468  pjoml3t 9472  osumlem5 9499  osumlem8 9502  osumt 9505  spansncv 9514  pjadjt 9547  pjaddt 9548  pjsubt 9550  pjmult 9551  pjcjt2 9554  hosubclt 9616  hoaddcomt 9617  hoaddasst 9625  hocsubdirt 9628  ho0subt 9640  honegsubt 9642  adjsymt 9676  eigre 9677  eigret 9678  eigpos 9679  eigorth 9680  eigortht 9681  cnopct 9753  lnoplt 9754  unopt 9755  hmopt 9762  cnfnct 9770  lnfnlt 9771  adjt 9773  adjvalvalt 9777  bravalt 9783  kbvalt 9792  eleigvect 9797  hoddit 9830  lnopeq0lem2 9846  lnopuni 9852  lnophm 9858  nmcopexlem4 9869  nmcopex 9872  nmcfnexlem4 9898  nmcfnex 9901  riesz3 9910  riesz4 9911  cnlnadjlem4 9918  cnlnadjlem5 9919  cnlnadj 9924  nmopadjle 9936  nmopco 9942  cnvbravalt 9956  leopg 9967  hmopidmch 9990  pjclem3 10035  hstel2t 10056  stjt 10072  mdbrt 10131  dmdbrt 10136  mdsl0 10145  chcv1t 10190  chjatom 10192  cvexcht 10209  atcvat4 10232  sumdmdlem 10252  cdjreu 10264  cdj1 10265  cdj3lem1 10266  cdj3lem2 10267  cdj3lem2b 10269  cdj3lem3b 10272  cdj3 10273  ghomgrpilem1 10290  ghomlin 10298  elgiso 10303  cayleylem2 10317  cayleythlem 10320  hmph 10411  iintlem1 10476  iintlem2 10477  1ded 10515  domcmpd 10523  codcmpd 10524  cmpasso 10550  cmpida 10551  ismonb2 10582  cmpmon 10585  icmpmon 10587  idmon 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950

Copyright terms: Public domain