Theorem opreq2 3967

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq2

Step	Hyp	Ref	Expression
1		opeq2 2486	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 3726	. 2 |- (A = B -> (F` <.C, A>.) = (F` <.C, B>.))
3		df-opr 3963	. 2 |- (CFA) = (F` <.C, A>.)
4		df-opr 3963	. 2 |- (CFB) = (F` <.C, B>.)
5	2, 3, 4	3eqtr4g 1530	1 |- (A = B -> (CFA) = (CFB))

Syntax hints:   -> wi 3   = wceq 956  <.cop 2409  ` cfv 3180  (class class class)co 3961

This theorem is referenced by:  opreq12 3968  opreq2i 3970  opreq2d 3974  rcla4eopr 3988  foprcl 4013  ndmoprcl 4042  caoprcl 4050  caoprcom 4051  caoprass 4052  caoprcan 4053  caoprord 4054  caoprdistr 4057  caoprmo 4068  curry1 4096  curry1val 4098  elrnoprabg 4122  omv 4149  oev 4151  oesuc 4164  oacl 4168  omcl 4169  oecl 4170  oa0r 4171  om0r 4172  om1r 4175  oe1m 4177  oaordi 4178  oaord 4179  oawordri 4182  oawordeulem 4186  oaass 4193  oarec 4194  omordi 4195  omord2 4196  omcan 4198  omwordri 4201  om00 4204  odi 4208  omass 4209  oen0 4211  oeordi 4212  oeord 4213  oecan 4214  oewordri 4217  oeworde 4218  oelim2 4220  nnacl 4227  nnmcl 4228  nnecl 4229  nnacom 4231  nnmsucr 4238  nnmcom 4239  oaabs 4250  nneob 4253  th3qlem2 4313  th3q 4315  ecoprcom 4317  ecoprass 4318  ecoprdi 4319  map0 4342  unfilem2 4539  unfilem3 4540  addcmpblnq 5040  addclpq 5046  mulclpq 5048  recmulpq 5058  dmrecpq 5062  ltapq 5064  ltmpq 5065  ltexpq 5068  ltbtwnpq 5072  ltrpq 5073  genpv 5090  genpass 5100  distrlem1pr 5115  1idpr 5121  prlem934 5127  ltexprlem3 5132  ltexprlem4 5133  ltexpri 5137  ltaprlem 5138  ltapr 5139  prlem936 5143  reclem3pr 5146  recexpr 5148  mulcmpblnrlem 5170  addclsr 5180  mulclsr 5181  ltasr 5197  negexsr 5199  recexsrlem 5200  mulgt0sr 5202  recexsr 5204  supsrlem2 5214  addcnsr 5241  mulcnsr 5242  axaddopr 5253  axmulopr 5254  axaddrcl 5260  axmulrcl 5262  axrnegex 5271  axrrecex 5272  axcnre 5274  pre-axltadd 5277  pre-axmulgt0 5278  cnegextlem1 5333  cnegext 5336  addcan 5339  addcant 5340  negeu 5343  negeq 5347  subclt 5355  subadd 5359  subaddt 5363  negsubt 5370  ine0 5422  1re 5423  mulneg1t 5439  mul2negt 5442  negdit 5443  ltadd2 5578  addge0 5587  add20 5590  mulge0 5595  msqge0 5602  ltadd1t 5611  leadd1t 5613  ltsubaddt 5615  lesubaddt 5617  lt2addt 5631  le2addt 5632  addgt0t 5634  addgegt0t 5635  addge0t 5637  lesub0t 5665  mulge0t 5666  recextlem2 5670  recext 5671  mulcan 5673  mulcant2 5674  mul0or 5677  mul0ort 5679  receu 5684  divmul 5688  divmulz 5689  divmult 5690  divclz 5694  divclt 5695  divcan1z 5701  divcan2z 5702  divcan1t 5703  divcan2t 5704  recne0z 5708  recne0t 5709  recidt 5712  divrecz 5715  divrect 5716  divdirz 5726  divdirt 5727  divdirtOLD 5728  divcan3t 5733  div11t 5736  recrect 5747  rec11i 5748  rec11 5749  redivcl 5769  redivclz 5770  redivclt 5771  eqneg 5775  ltmul1 5793  ltdiv1 5795  prodgt0t 5797  prodge0t 5799  ltmul1t 5801  lemul1it 5808  lemul1itOLD 5809  ltdiv1t 5820  ltdiv1tOLD 5821  ltmuldivt 5834  ltmuldivtOLD 5835  ltrec 5847  lt2msq 5849  ltrect 5852  lerect 5853  nnaddclt 5908  nnmulclt 5909  nnsubt 5925  nndivt 5927  2timest 5972  nn0addclt 6088  nn0mulcl 6090  nn0mulclt 6091  nnnn0addclt 6093  nn0subt 6129  quorem 6218  zqt 6224  qrecclt 6237  seq1rn2 6285  ser1ft 6292  shftfval 6306  icoshftf1olem 6370  icoun 6373  snunioo 6375  uzaddclt 6409  fzrevralt 6479  fzshftralt 6482  fsequb 6483  seqzfveq 6514  seqzrn2 6516  dfseq0 6523  expp1t 6534  expcllem 6535  1expt 6544  expeq0t 6545  expne0it 6548  expgt0t 6549  expge0t 6551  expgt1t 6552  expge1t 6553  mulexpt 6554  recexpt 6555  expaddt 6556  expmult 6557  expcant 6561  expwordit 6563  expmwordit 6566  exple1t 6567  sqlecant 6601  binom2t 6610  bernneq 6612  expnbndt 6614  discrlem2 6617  discrlem 6619  nn0opth2t 6628  sqrlem21 6653  sqrmul 6665  sqr2irrlem5 6688  cru 6697  crut 6698  crne0 6699  creur 6702  creui 6703  replimt 6721  reim0bt 6735  rereb 6738  readdt 6763  imaddt 6766  cjaddt 6770  cjmult 6771  cjexpt 6775  abs00 6800  absmult 6816  absdivt 6818  absexpt 6826  cjdivt 6847  abssubt 6852  abstrit 6856  abs1m 6862  recant 6863  abs3lemt 6865  ser1absdiflem 6887  facdivt 6900  faclbnd3 6905  faclbnd4lem1 6906  faclbnd4lem2 6907  faclbnd4lem3 6908  faclbnd4lem4 6909  faclbnd6 6912  bcvalt 6916  bcpasc2t 6926  bcpasc 6927  bcpasct 6928  bccl2t 6929  clim 6935  fsump1slem 6970  fsumcllem 6972  fsum1ps 6976  fsumsplit 6978  fsumadd 6980  csbfsumlem 6984  fsumcom 6986  fsumrev 6987  fsumshft 6989  fsummulc1 6991  fsumconst 6996  fsumcmp 6998  fsumcmpndx2 7000  fsumabs 7001  binomlem1 7024  binomlem2 7025  binomlem3 7026  binomlem4 7027  binomlem6 7029  binom 7030  bcxmaslem1 7032  bcxmas 7034  cvgcmp3cetlem1 7146  cvgcmp3cetlem2 7147  infcvg 7182  expcnvlem3 7187  geoser 7192  geolimilem 7193  geolim 7195  geolim1i 7196  geolim1 7197  cvgratlem1ALT 7205  cvgratlem2ALT 7206  cvgratlem1 7208  cvgratlem5 7212  fsum0diaglem2 7215  fsum0diag 7216  fsum0diag2 7217  fsum0diag4 7219  mulc1cncf 7237  ivthlem6 7244  ivthlem7 7245  efcltlem1 7262  dfef2 7265  ef0lem 7268  efclt 7270  efcvg 7272  eftval 7274  erelem2 7278  erelem3 7279  erelem6 7282  efaddlem6 7301  efaddlem24 7319  efaddlem26 7321  efaddlem27 7322  efaddt 7325  efexpt 7330  ef1tllem 7339  ef01tlub 7344  absef01tlub 7346  eirr 7352  ef4pt 7358  eflegeolem2 7371  eflegeot 7373  efm1legeot 7375  efcnlem4 7379  sinvalt 7386  cosvalt 7387  sinaddt 7410  cosaddt 7411  abseft 7440  demoivre 7441  acdc2lem1 7445  acdc5lem1 7448  infpnlem2 7464  ruclem4 7470  ruclem32 7498  infmap2 7538  retopbas 7612  meteq0 7769  mettri2 7770  mettri4 7771  elbl 7795  blelrn 7805  blss 7810  ssblex 7813  blnei 7836  metcnp 7844  blssioo 7870  tgioolem 7871  lmbr 7885  fsumcnlem 7946  bcthlem15 7970  bcthlem17 7972  isgrp 7998  grpass 8004  grpidinvlem1 8005  grpidinvlem3 8007  grpidinvlem4 8008  grpidinv 8009  grpideu 8010  grpidinv2 8017  grprcan 8020  grpinvval 8024  grpinv 8026  grpinvid1 8029  grplcan 8032  isgrp2i 8033  grplactval 8054  grplactf1o 8055  ablcom 8060  issubgilem 8078  grpsn 8081  ablsn 8082  ghgrpilem1 8090  ghgrpilem3 8092  ghgrpilem4 8093  ghgrpi 8094  ringid 8102  ringdi 8103  ringdir 8104  ringass 8105  cnring 8119  ringsn 8120  vcid 8127  vcdi 8128  vcdir 8129  vcass 8130  nvmul0or 8229  nvs 8247  nvtri 8255  sm1cnilem 8304  ipval 8310  lnolin 8372  bloval 8398  nmlno0 8412  blocnilem 8421  phpar2 8439  phpar 8440  ipdiri 8446  ipassi 8458  siilem1 8468  siii 8470  sii 8471  ip2eqi 8474  ajfun 8478  minveclem13 8514  minvecex 8535  minveceu 8540  minvecdist 8542  minveclem39 8544  htthlem2 8578  sincolem 8622  efgh 8673  efghgrpilem 8674  efif 8676  efifo 8684  efif1lem6 8690  efif1 8692  shftefif1olem 8696  eff1i 8699  effoi 8700  hvsubvalt 8841  hvmul0ort 8849  hvsubsub4t 8882  hvaddcan 8887  hvnegdit 8889  hvsubeq0t 8890  hvaddcant 8892  hvsubaddt 8899  hial0 8923  hial02 8924  hial2eqt 8927  normlem6 8936  normlem9at 8942  normsub0t 8958  norm-iit 8960  norm-iiit 8962  normsubt 8965  normpytht 8967  norm3dift 8972  norm3lemt 8974  norm3adift 8975  normpart 8977  polidt 8981  bcst 9003  hlim 9011  hlim2 9015  shaddclt 9040  shaddcltOLD 9041  shmulclt 9042  shmulcltOLD 9043  hsn0elch 9075  ocsh 9111  ocorth 9119  ocin 9124  occllem2 9129  occllem7 9134  occllem8 9135  projlem1 9141  projlem7 9147  projlem17 9157  projlem20 9160  projlem22 9162  projlem26 9166  projlem28 9168  pjthlem13 9186  pjthlem14 9187  pjtheu 9190  omlsi 9200  pjoc1 9219  shsel3t 9234  shscl 9236  shsclt 9237  choc0 9245  shslejt 9305  shlubt 9309  chlejb1t 9390  chnlet 9392  chjasst 9411  ledit 9418  h1deot 9427  h1de2 9431  elspansnt 9444  elspansn2t 9445  spanunsn 9457  h1datom 9459  pjoml6 9487  cmbr3t 9506  pjoml3t 9510  osumlem5 9537  osumlem8 9540  osumt 9543  spansncv 9552  pjadjt 9585  pjaddt 9586  pjsubt 9588  pjmult 9589  pjcjt2 9592  hosubclt 9654  hoaddcomt 9655  hoaddasst 9663  hocsubdirt 9666  ho0subt 9678  honegsubt 9680  adjsymt 9714  eigre 9715  eigret 9716  eigpos 9717  eigorth 9718  eigortht 9719  cnopct 9792  lnoplt 9793  unopt 9794  hmopt 9801  cnfnct 9809  lnfnlt 9810  adjt 9812  adjvalvalt 9816  bravalt 9822  kbvalt 9831  eleigvect 9836  hoddit 9870  lnopeq0lem2 9886  lnopuni 9892  lnophm 9898  nmcopexlem4 9909  nmcopex 9912  nmcfnexlem4 9938  nmcfnex 9941  riesz3 9950  riesz4 9951  cnlnadjlem4 9958  cnlnadjlem5 9959  cnlnadj 9964  nmopadjle 9976  nmopco 9983  cnvbravalt 9998  leopg 10010  hmopidmch 10034  pjclem3 10080  hstel2t 10101  stjt 10117  mdbrt 10176  dmdbrt 10181  mdsl0 10192  chcv1t 10237  chjatom 10239  cvexcht 10256  atcvat4 10279  sumdmdlem 10300  cdjreu 10314  cdj1 10315  cdj3lem1 10316  cdj3lem2 10317  cdj3lem2b 10319  cdj3lem3b 10322  cdj3 10323  ghomgrpilem1 10340  ghomlin 10348  elgiso 10353  cayleylem2 10365  cayleythlem 10368  hmph 10466  iintlem1 10544  iintlem2 10545  1ded 10583  domcmpd 10591  codcmpd 10592  cmpasso 10618  cmpida 10619  ismonb2 10650  cmpmon 10653  icmpmon 10655  idmon 10656

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 2701  ax-pow 2740  ax-pr 2777

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 1586  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-pw 2400  df-sn 2410  df-pr 2411  df-op 2414  df-uni 2502  df-br 2618  df-opab 2665  df-xp 3182  df-cnv 3184  df-dm 3186  df-rn 3187  df-res 3188  df-ima 3189  df-fv 3196  df-opr 3963

Copyright terms: Public domain