Theorem opreq2 4027

Description: Equality theorem for operation value.

Assertion

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

Proof of Theorem opreq2

Step	Hyp	Ref	Expression
1		opeq2 2542	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 3785	. 2 |- (A = B -> (F` <.C, A>.) = (F` <.C, B>.))
3		df-opr 4023	. 2 |- (CFA) = (F` <.C, A>.)
4		df-opr 4023	. 2 |- (CFB) = (F` <.C, B>.)
5	2, 3, 4	3eqtr4g 1578	1 |- (A = B -> (CFA) = (CFB))

Syntax hints:   -> wi 3   = wceq 997  <.cop 2463  ` cfv 3239  (class class class)co 4021

This theorem is referenced by:  opreq12 4028  opreq2i 4030  opreq2d 4034  rcla4eopr 4048  foprcl 4073  ndmoprcl 4102  caoprcl 4110  caoprcom 4111  caoprass 4112  caoprcan 4113  caoprord 4114  caoprdistr 4117  caoprmo 4128  curry1 4156  curry1val 4158  elrnoprabg 4182  omv 4209  oev 4211  oesuc 4224  oacl 4228  omcl 4229  oecl 4230  oa0r 4231  om0r 4232  om1r 4235  oe1m 4237  oaordi 4238  oaord 4239  oawordri 4242  oawordeulem 4246  oaass 4253  oarec 4254  omordi 4255  omord2 4256  omcan 4258  omwordri 4261  om00 4264  odi 4268  omass 4269  oen0 4271  oeordi 4272  oeord 4273  oecan 4274  oewordri 4277  oeworde 4278  oelim2 4280  nnacl 4287  nnmcl 4288  nnecl 4289  nnacom 4291  nnmsucr 4298  nnmcom 4299  oaabs 4310  nneob 4313  th3qlem2 4376  th3q 4378  ecoprcom 4380  ecoprass 4381  ecoprdi 4382  map0 4405  unfilem2 4612  unfilem3 4613  addcmpblnq 5117  addclpq 5123  mulclpq 5125  recmulpq 5135  dmrecpq 5139  ltapq 5141  ltmpq 5142  ltexpq 5145  ltbtwnpq 5149  ltrpq 5150  genpv 5167  genpass 5177  distrlem1pr 5192  1idpr 5198  prlem934 5204  ltexprlem3 5209  ltexprlem4 5210  ltexpri 5214  ltaprlem 5215  ltapr 5216  prlem936 5220  reclem3pr 5223  recexpr 5225  mulcmpblnrlem 5247  addclsr 5257  mulclsr 5258  ltasr 5274  negexsr 5276  recexsrlem 5277  mulgt0sr 5279  recexsr 5281  supsrlem2 5291  addcnsr 5318  mulcnsr 5319  axaddopr 5330  axmulopr 5331  axaddrcl 5337  axmulrcl 5339  axrnegex 5348  axrrecex 5349  axcnre 5351  pre-axltadd 5354  pre-axmulgt0 5355  cnegexlem1 5410  cnegex 5413  addcani 5416  addcan 5417  negeui 5420  negeq 5424  subcl 5432  subaddi 5436  subadd 5440  negsub 5447  ine0 5499  1re 5500  mulneg1 5516  mul2neg 5519  negdi 5520  ltadd2i 5655  addge0i 5664  add20i 5667  mulge0i 5672  msqge0i 5679  ltadd1 5688  leadd1 5690  ltsubadd 5692  lesubadd 5694  lt2add 5708  le2add 5709  addgt0 5712  addgegt0 5713  addge0 5715  lesub0 5743  mulge0 5744  recextlem2 5748  recex 5749  mulcani 5751  mulcaniOLD 5752  mulcant2i 5753  mulcant2iOLD 5754  mul0ori 5759  mul0or 5761  receui 5766  divmuli 5770  divmulzi 5771  divmul 5772  divmulOLD 5773  divclzi 5779  divcl 5780  divcan1zi 5786  divcan2zi 5787  divcan1 5788  recne0zi 5793  recne0 5794  recid 5797  divreczi 5800  divrec 5801  divdirzi 5812  divdir 5813  divdirOLD 5814  divcan3 5819  div11 5822  recrec 5834  rec11ii 5835  rec11i 5836  redivcli 5856  redivclzi 5857  redivcl 5858  eqnegi 5862  ltmul1i 5880  ltdiv1i 5882  prodgt0 5884  prodge0 5886  ltmul1 5888  lemul1a 5895  lemul1aOLD 5896  ltdiv1 5907  ltdiv1OLD 5908  ltmuldiv 5921  ltmuldivOLD 5922  ltreci 5939  lt2msqi 5941  ltrec 5944  lerec 5945  nnaddcl 6000  nnmulcl 6001  nnsub 6018  nndiv 6020  2times 6065  nn0addcl 6202  nn0mulcli 6204  nn0mulcl 6205  nnnn0addcl 6207  nn0sub 6243  zdiv 6270  zq 6312  qreccl 6325  modval 6372  icoshftf1olem 6436  icoun 6439  snunioo 6441  uzaddcl 6475  fzrevral 6545  fzshftral 6548  fsequb 6549  seq1rn2 6580  ser1f 6587  shftfval 6601  seqzfveq 6643  seqzrn2 6645  dfseq0 6652  expp1 6663  expcllem 6664  1exp 6673  expeq0 6674  expne0i 6677  expgt0 6678  expge0 6680  expgt1 6681  expge1 6682  mulexp 6683  recexp 6684  expadd 6685  expmul 6686  expcan 6690  expwordi 6692  expmwordi 6695  exple1 6696  sqlecan 6730  binom2 6739  bernneq 6741  expnbnd 6743  discrlem2 6747  discrlem 6749  nn0opth2 6758  sqrlem21 6783  sqrmuli 6795  sqr2irrlem5 6818  crui 6827  cru 6828  crne0i 6829  creur 6832  creui 6833  replim 6851  reim0b 6865  readd 6895  imadd 6898  cjadd 6902  cjmul 6903  cjexp 6907  abs00i 6932  absmul 6948  absdiv 6950  absexp 6958  cjdiv 6979  abssub 6984  abstri 6988  abs1mi 6994  recan 6995  abs3lem 6997  ser1absdiflem 7019  facdiv 7032  faclbnd3 7037  faclbnd4lem1 7038  faclbnd4lem2 7039  faclbnd4lem3 7040  faclbnd4lem4 7041  faclbnd6 7044  bcval 7048  bcpasc2 7058  bcpasci 7059  bcpasc 7060  bccl2 7061  clim 7067  fsump1slem 7102  fsumcllem 7104  fsum1ps 7108  fsumspl 7110  fsumadd 7112  csbfsumlem 7116  fsumcom 7118  fsumrev 7119  fsumshf 7121  fsummulc1 7123  fsumcons 7128  fsumcmp 7130  fsumcmpndx2 7132  fsumabs 7133  binomlem1 7156  binomlem2 7157  binomlem3 7158  binomlem4 7159  binomlem6 7161  binomi 7162  bcxmaslem1 7164  bcxmas 7166  cvgcmp3cetlem1 7278  cvgcmp3cetlem2 7279  infcvgi 7314  expcnvlem3 7319  geoseri 7324  geolimilem 7325  geolim 7327  geolim1i 7328  geolim1 7329  cvgratlem1ALT 7337  cvgratlem2ALT 7338  cvgratlem1 7340  cvgratlem5 7344  fsum0diaglem2 7347  fsum0diag 7348  fsum0diag2 7349  fsum0diag4 7351  mulc1cncf 7369  ivthlem6 7376  ivthlem7 7377  efcltlem1 7394  dfef2i 7397  ef0lem 7400  efcl 7402  efcvg 7404  eftval 7406  erelem2 7410  erelem3 7411  erelem6 7414  efaddlem6 7433  efaddlem24 7451  efaddlem26 7453  efaddlem27 7454  efadd 7457  efexp 7462  ef1tllem 7471  ef01tlubi 7476  absef01tlubi 7478  eirr 7484  ef4p 7491  eflegeolem2 7505  eflegeo 7507  efm1legeo 7509  efcnlem4 7513  sinval 7520  cosval 7521  sinadd 7544  cosadd 7545  absef 7575  demoivre 7576  acdc2lem1 7580  acdc5lem1 7583  infpnlem2 7599  ruclem4 7605  ruclem32 7633  infmap2 7673  retopbas 7740  meteq0 7897  mettri2 7898  mettri4 7899  elbl 7923  blelrn 7933  blss 7938  ssblex 7941  blnei 7964  metcnp 7972  blssioo 7998  tgioolem 7999  lmbr 8013  fsumcnlem 8074  bcthlem15 8098  bcthlem17 8100  isgrp 8126  grpass 8132  grpidinvlem1 8133  grpidinvlem3 8135  grpidinvlem4 8136  grpidinv 8137  grpideu 8138  grpidinv2 8144  grprcan 8147  grpinvval 8151  grpinv 8153  grpinvid1 8156  grplcan 8159  isgrp2i 8160  grplactval 8181  grplactf1o 8182  ablcom 8187  issubgilem 8205  grpsn 8208  ablsn 8209  ghgrpilem1 8217  ghgrpilem3 8219  ghgrpilem4 8220  ghgrpi 8221  ringid 8229  ringdi 8230  ringdir 8231  ringass 8232  cnring 8246  ringsn 8247  vcid 8254  vcdi 8255  vcdir 8256  vcass 8257  nvmul0or 8356  nvs 8374  nvtri 8382  sm1cnilem 8431  ipval 8437  lnolin 8499  bloval 8525  nmlno0 8539  blocnilem 8548  phpar2 8566  phpar 8567  ipdiri 8573  ipassi 8585  siilem1 8595  siii 8597  sii 8598  ip2eqi 8601  ajfun 8605  minveclem13 8641  minvecex 8662  minveceu 8667  minvecdist 8669  minveclem39 8671  htthlem2 8705  sincolem 8748  efgh 8801  efghgrpilem 8802  efif 8804  efifo 8812  efif1lem6 8818  efif1 8820  shftefif1olem 8824  eff1i 8827  effoi 8828  hvsubval 8969  hvmul0or 8977  hvsubsub4 9010  hvaddcani 9015  hvnegdi 9017  hvsubeq0 9018  hvaddcan 9020  hvsubadd 9027  hial0 9051  hial02 9052  hial2eq 9055  normlem6 9064  normlem9at 9070  normsub0 9086  norm-ii 9088  norm-iii 9090  normsub 9093  normpyth 9095  norm3dif 9100  norm3lemt 9102  norm3adifi 9103  normpar 9105  polid 9109  bcs 9131  hlimi 9139  hlim2 9143  shaddcl 9168  shaddclOLD 9169  shmulcl 9170  shmulclOLD 9171  hsn0elch 9203  ocsh 9239  ocorth 9247  ocin 9252  occllem2 9257  occllem7 9262  occllem8 9263  projlem1 9269  projlem7 9275  projlem17 9285  projlem20 9288  projlem22 9290  projlem26 9294  projlem28 9296  pjthlem13 9314  pjthlem14 9315  pjtheui 9318  omlsii 9328  pjoc1i 9347  shsel3 9362  shscli 9364  shscl 9365  choc0 9373  shslej 9433  shlub 9437  chlejb1 9518  chnle 9520  chjass 9539  ledi 9546  h1deoi 9555  h1de2i 9559  elspansn 9572  elspansn2 9573  spanunsni 9585  h1datomi 9587  pjoml6i 9615  cmbr3 9634  pjoml3 9638  osumlem5 9665  osumlem8 9668  osum 9671  spansncvi 9680  pjadji 9713  pjaddi 9714  pjsubi 9716  pjmuli 9717  pjcjt2 9720  hosubcl 9782  hoaddcom 9783  hoaddass 9791  hocsubdir 9794  ho0sub 9806  honegsub 9808  adjsym 9842  eigrei 9843  eigre 9844  eigposi 9845  eigorthi 9846  eigorth 9847  cnopc 9920  lnopl 9921  unop 9922  hmop 9929  cnfnc 9937  lnfnl 9938  adj1 9940  adjvalval 9944  braval 9950  kbval 9959  eleigvec 9964  hoddi 9998  lnopeq0lem2 10014  lnopunii 10020  lnophmi 10026  nmcopexlem4 10037  nmcopexi 10040  nmcfnexlem4 10066  nmcfnexi 10069  riesz3i 10078  riesz4i 10079  cnlnadjlem4 10086  cnlnadjlem5 10087  cnlnadji 10092  nmopadjlei 10104  nmopcoi 10111  cnvbraval 10126  leopg 10138  hmopidmchi 10162  pjclem3 10209  hstel2 10230  stj 10246  mdbr 10305  dmdbr 10310  mdsl0 10321  chcv1 10366  chjatom 10368  cvexch 10385  atcvat4i 10408  sumdmdlem 10429  cdjreui 10443  cdj1i 10444  cdj3lem1 10445  cdj3lem2 10446  cdj3lem2b 10448  cdj3lem3b 10451  cdj3i 10452  ghomgrpilem1 10470  ghomlin 10478  elgiso 10483  cayleylem2 10495  cayleythlem 10498  hmph 10618  iintlem1 10714  iintlem2 10715  1ded 10753  domcmpd 10761  codcmpd 10762  cmpasso 10788  cmpida 10789  ismonb2 10822  cmpmon 10825  icmpmon 10826  idmon 10827  isepib 10830

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-xp 3241  df-cnv 3243  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fv 3255  df-opr 4023

Copyright terms: Public domain