Theorem opreq2 3960

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq2

Step	Hyp	Ref	Expression
1		opeq2 2484	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 3719	. 2 |- (A = B -> (F` <.C, A>.) = (F` <.C, B>.))
3		df-opr 3956	. 2 |- (CFA) = (F` <.C, A>.)
4		df-opr 3956	. 2 |- (CFB) = (F` <.C, B>.)
5	2, 3, 4	3eqtr4g 1528	1 |- (A = B -> (CFA) = (CFB))

Syntax hints:   -> wi 3   = wceq 954  <.cop 2407  ` cfv 3177  (class class class)co 3954

This theorem is referenced by:  opreq12 3961  opreq2i 3963  opreq2d 3967  rcla4eopr 3981  foprcl 4006  ndmoprcl 4036  caoprcl 4044  caoprcom 4045  caoprass 4046  caoprcan 4047  caoprord 4048  caoprdistr 4051  caoprmo 4062  curry1 4088  curry1val 4090  elrnoprabg 4114  omv 4141  oev 4143  oesuc 4156  oacl 4160  omcl 4161  oecl 4162  oa0r 4163  om0r 4164  om1r 4167  oe1m 4169  oaordi 4170  oaord 4171  oawordri 4174  oawordeulem 4178  oaass 4185  oarec 4186  omordi 4187  omord2 4188  omcan 4190  omwordri 4193  om00 4196  odi 4200  omass 4201  oen0 4203  oeordi 4204  oeord 4205  oecan 4206  oewordri 4209  oeworde 4210  oelim2 4212  nnacl 4219  nnmcl 4220  nnecl 4221  nnacom 4223  nnmsucr 4230  nnmcom 4231  oaabs 4242  nneob 4245  th3qlem2 4305  th3q 4307  ecoprcom 4309  ecoprass 4310  ecoprdi 4311  map0 4334  unfilem2 4531  unfilem3 4532  addcmpblnq 5032  addclpq 5038  mulclpq 5040  recmulpq 5050  dmrecpq 5054  ltapq 5056  ltmpq 5057  ltexpq 5060  ltbtwnpq 5064  ltrpq 5065  genpv 5082  genpass 5092  distrlem1pr 5107  1idpr 5113  prlem934 5119  ltexprlem3 5124  ltexprlem4 5125  ltexpri 5129  ltaprlem 5130  ltapr 5131  prlem936 5135  reclem3pr 5138  recexpr 5140  mulcmpblnrlem 5162  addclsr 5172  mulclsr 5173  ltasr 5189  negexsr 5191  recexsrlem 5192  mulgt0sr 5194  recexsr 5196  supsrlem2 5206  addcnsr 5233  mulcnsr 5234  axaddopr 5245  axmulopr 5246  axaddrcl 5252  axmulrcl 5254  axrnegex 5263  axrrecex 5264  axcnre 5266  pre-axltadd 5269  pre-axmulgt0 5270  cnegextlem1 5325  cnegext 5328  addcan 5331  addcant 5332  negeu 5335  negeq 5339  subclt 5347  subadd 5351  subaddt 5355  negsubt 5362  ine0 5414  1re 5415  mulneg1t 5431  mul2negt 5434  negdit 5435  ltadd2 5572  addge0 5581  add20 5584  mulge0 5589  msqge0 5596  ltadd1t 5605  leadd1t 5607  ltsubaddt 5609  lesubaddt 5611  lt2addt 5625  le2addt 5626  addgt0t 5628  addgegt0t 5629  addge0t 5631  lesub0t 5659  mulge0t 5660  recextlem2 5664  recext 5665  mulcan 5667  mulcant2 5668  mul0or 5671  mul0ort 5673  receu 5678  divmul 5682  divmulz 5683  divmult 5684  divclz 5688  divclt 5689  divcan1z 5695  divcan2z 5696  divcan1t 5697  divcan2t 5698  recne0z 5702  recne0t 5703  recidt 5706  divrecz 5709  divrect 5710  divdirz 5720  divdirt 5721  divcan3t 5726  div11t 5729  recrect 5740  rec11i 5741  rec11 5742  redivcl 5762  redivclz 5763  redivclt 5764  eqneg 5768  ltmul1 5786  ltdiv1 5788  prodgt0t 5790  prodge0t 5792  ltmul1t 5794  lemul1it 5801  lemul1itOLD 5802  ltdiv1t 5813  ltmuldivt 5825  ltrec 5835  lt2msq 5837  ltrect 5840  lerect 5841  nnaddclt 5896  nnmulclt 5897  nnsubt 5912  nndivt 5914  2timest 5959  nn0addclt 6075  nn0mulcl 6077  nn0mulclt 6078  nnnn0addclt 6080  nn0subt 6116  zqt 6206  qrecclt 6219  seq1rn2 6266  ser1ft 6273  shftfval 6287  icoshftf1olem 6351  icoun 6354  snunioo 6356  uzaddclt 6389  fzrevralt 6459  fzshftralt 6462  fsequb 6463  seqzfveq 6494  seqzrn2 6496  dfseq0 6503  expp1t 6514  expcllem 6515  1expt 6524  expeq0t 6525  expne0it 6527  expgt0t 6528  expge0t 6530  expgt1t 6531  expge1t 6532  mulexpt 6533  recexpt 6534  expaddt 6535  expmult 6536  expcant 6540  expwordit 6542  expmwordit 6545  exple1t 6546  sqlecant 6580  binom2t 6589  bernneq 6591  expnbndt 6593  discrlem2 6595  discrlem 6597  nn0opth2t 6606  sqrlem21 6631  sqrmul 6643  sqr2irrlem5 6666  cru 6675  crut 6676  crne0 6678  creur 6681  creui 6682  replimt 6700  readdt 6748  imaddt 6751  cjaddt 6755  cjmult 6756  cjexpt 6760  absmult 6801  absdivt 6803  absexpt 6811  cjdivt 6835  abssubt 6840  abstrit 6843  abs1m 6849  recant 6850  abs3lemt 6852  ser1absdiflem 6874  facdivt 6887  faclbnd3 6892  faclbnd4lem1 6893  faclbnd4lem2 6894  faclbnd4lem3 6895  faclbnd4lem4 6896  faclbnd6 6899  bcvalt 6903  bcpasc2t 6914  bcpasc 6915  bcpasct 6916  bccl2t 6917  clim 6923  fsump1slem 6958  fsumcllem 6960  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  csbfsumlem 6972  fsumcom 6974  fsumrev 6975  fsumshft 6977  fsummulc1 6979  fsumconst 6984  fsumcmp 6986  fsumcmpndx2 6988  fsumabs 6989  binomlem1 7012  binomlem2 7013  binomlem3 7014  binomlem4 7015  binomlem6 7017  binom 7018  bcxmaslem1 7020  bcxmas 7022  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  infcvg 7167  expcnvlem3 7172  geoser 7177  geolimilem 7178  geolim 7180  geolim1i 7181  geolim1 7182  cvgratlem1ALT 7190  cvgratlem2ALT 7191  cvgratlem1 7193  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag 7201  fsum0diag2 7202  fsum0diag4 7204  mulc1cncf 7222  ivthlem6 7229  ivthlem7 7230  ivthlem6OLD 7238  ivthlem7OLD 7239  efcltlem1 7254  dfef2 7257  ef0lem 7260  efclt 7262  efcvg 7264  eftval 7266  erelem2 7270  erelem3 7271  erelem6 7274  efaddlem6 7293  efaddlem24 7311  efaddlem26 7313  efaddlem27 7314  efaddt 7317  efexpt 7322  ef1tllem 7331  ef01tlub 7335  absef01tlub 7337  eirr 7343  ef4pt 7349  eflegeolem2 7362  eflegeot 7364  efm1legeot 7366  efcnlem4 7370  sinvalt 7379  cosvalt 7380  sinaddt 7403  cosaddt 7404  abseft 7433  demoivre 7434  acdc2lem1 7438  acdc5lem1 7441  infpnlem2 7458  ruclem4 7464  ruclem32 7492  infmap2 7531  retopbas 7605  meteq0 7762  mettri2 7763  mettri4 7764  elbl 7790  blelrn 7800  blss 7805  ssblex 7808  blnei 7831  metcnp 7839  blssioo 7865  tgioolem 7866  lmbr 7880  fsumcnlem 7939  bcthlem15 7963  bcthlem17 7965  isgrp 7991  grpass 7997  grpidinvlem1 7998  grpidinvlem3 8000  grpidinvlem4 8001  grpidinv 8002  grpideu 8003  grpidinv2 8010  grprcan 8013  grpinvval 8017  grpinv 8019  grpinvid1 8022  grplcan 8025  isgrp2i 8026  grplactval 8048  grplactf1o 8049  ablcom 8054  issubgilem 8073  grpsn 8076  ablsn 8077  ghgrpilem1 8085  ghgrpilem3 8087  ghgrpilem4 8088  ghgrpi 8089  ringid 8097  ringdi 8098  ringdir 8099  ringass 8100  cnring 8114  ringsn 8115  vcid 8122  vcdi 8123  vcdir 8124  vcass 8125  nvmul0or 8224  nvs 8242  nvtri 8250  sm1cnilem 8294  ipval 8300  lnolin 8362  bloval 8386  nmlno0 8400  blocnilem 8408  phpar2 8426  phpar 8427  ipdiri 8433  ipassi 8445  siilem1 8455  siii 8457  sii 8458  ip2eqi 8461  ajfun 8465  minveclem13 8501  minvecex 8522  minveceu 8527  minvecdist 8529  minveclem39 8531  htthlem2 8564  sincolem 8603  efgh 8652  efghgrpilem 8653  efif 8655  efifo 8663  efif1lem6 8669  efif1 8671  shftefif1olem 8680  eff1i 8683  effoi 8684  hvsubvalt 8825  hvmul0ort 8833  hvsubsub4t 8866  hvaddcan 8871  hvnegdit 8873  hvsubeq0t 8874  hvaddcant 8876  hvsubaddt 8883  hial0 8907  hial02 8908  hial2eqt 8911  normlem6 8920  normlem9at 8926  normsub0t 8942  norm-iit 8944  norm-iiit 8946  normsubt 8949  normpytht 8951  norm3dift 8956  norm3lemt 8958  norm3adift 8959  normpart 8961  polidt 8965  bcst 8987  hlim 8995  hlim2 8999  shaddclt 9024  shaddcltOLD 9025  shmulclt 9026  shmulcltOLD 9027  hsn0elch 9059  ocsh 9095  ocorth 9103  ocin 9108  occllem2 9113  occllem7 9118  occllem8 9119  projlem1 9125  projlem7 9131  projlem17 9141  projlem20 9144  projlem22 9146  projlem26 9150  projlem28 9152  pjthlem13 9169  pjthlem14 9170  pjtheu 9173  omlsi 9183  pjoc1 9202  shsel3t 9217  shscl 9219  shsclt 9220  choc0 9228  shslejt 9288  shlubt 9292  chlejb1t 9373  chnlet 9375  chjasst 9394  ledit 9401  h1deot 9410  h1de2 9414  elspansnt 9428  elspansn2t 9429  spanunsn 9442  h1datom 9444  pjoml6 9472  cmbr3t 9491  pjoml3t 9495  osumlem5 9522  osumlem8 9525  osumt 9528  spansncv 9537  pjadjt 9570  pjaddt 9571  pjsubt 9573  pjmult 9574  pjcjt2 9577  hosubclt 9639  hoaddcomt 9640  hoaddasst 9648  hocsubdirt 9651  ho0subt 9663  honegsubt 9665  adjsymt 9699  eigre 9700  eigret 9701  eigpos 9702  eigorth 9703  eigortht 9704  cnopct 9776  lnoplt 9777  unopt 9778  hmopt 9785  cnfnct 9793  lnfnlt 9794  adjt 9796  adjvalvalt 9800  bravalt 9806  kbvalt 9815  eleigvect 9820  hoddit 9853  lnopeq0lem2 9869  lnopuni 9875  lnophm 9881  nmcopexlem4 9892  nmcopex 9895  nmcfnexlem4 9921  nmcfnex 9924  riesz3 9933  riesz4 9934  cnlnadjlem4 9941  cnlnadjlem5 9942  cnlnadj 9947  nmopadjle 9959  nmopco 9966  cnvbravalt 9981  leopg 9993  hmopidmch 10017  pjclem3 10063  hstel2t 10084  stjt 10100  mdbrt 10159  dmdbrt 10164  mdsl0 10174  chcv1t 10219  chjatom 10221  cvexcht 10238  atcvat4 10261  sumdmdlem 10281  cdjreu 10293  cdj1 10294  cdj3lem1 10295  cdj3lem2 10296  cdj3lem2b 10298  cdj3lem3b 10301  cdj3 10302  ghomgrpilem1 10319  ghomlin 10327  elgiso 10332  cayleylem2 10344  cayleythlem 10347  hmph 10447  iintlem1 10512  iintlem2 10513  1ded 10551  domcmpd 10559  codcmpd 10560  cmpasso 10586  cmpida 10587  ismonb2 10618  cmpmon 10621  icmpmon 10623  idmon 10624

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193  df-opr 3956

Copyright terms: Public domain