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 2553	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 3839	. 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 1574	1 |- (A = B -> (CFA) = (CFB))

Syntax hints:   -> wi 3   = wceq 992  <.cop 2469  ` cfv 3263  (class class class)co 4021

This theorem is referenced by:  opreq12 4028  opreq2i 4030  opreq2d 4034  rcla4eopr 4048  foprcl 4075  ndmoprcl 4105  caoprcl 4113  caoprcom 4114  caoprass 4115  caoprcan 4116  caoprord 4117  caoprdistr 4120  caoprmo 4131  elrnoprabg 4186  curry1 4193  curry1val 4195  onopruni 4210  onopriun 4211  omv 4287  oev 4289  oesuc 4302  oacl 4306  omcl 4307  oecl 4308  oa0r 4309  om0r 4310  om1r 4313  oe1m 4315  oaordi 4316  oaord 4317  oawordri 4320  oawordeulem 4324  oaass 4331  oarec 4332  omordi 4333  omord2 4334  omcan 4336  omwordri 4339  om00 4342  odi 4346  omass 4347  oen0 4349  oeordi 4350  oeord 4351  oecan 4352  oewordri 4355  oeworde 4356  oelim2 4358  oeoalem 4359  oeoa 4360  oeoelem 4361  oeoe 4362  nnacl 4369  nnmcl 4370  nnecl 4371  nnacom 4373  nnmsucr 4380  nnmcom 4381  oaabs 4392  nneob 4395  th3qlem2 4456  th3q 4458  ecoprcom 4460  ecoprass 4461  ecoprdi 4462  map0 4485  unfilem2 4695  unfilem3 4696  cdaung 5073  cdaeng 5076  nnacda 5090  addcmpblnq 5206  addclpq 5212  mulclpq 5214  recmulpq 5224  dmrecpq 5228  ltapq 5230  ltmpq 5231  ltexpq 5234  ltbtwnpq 5238  ltrpq 5239  genpv 5256  genpass 5266  distrlem1pr 5281  1idpr 5287  prlem934 5293  ltexprlem3 5298  ltexprlem4 5299  ltexpri 5303  ltaprlem 5304  ltapr 5305  prlem936 5309  reclem3pr 5312  recexpr 5314  mulcmpblnrlem 5336  addclsr 5346  mulclsr 5347  ltasr 5363  negexsr 5365  recexsrlem 5366  mulgt0sr 5368  recexsr 5370  supsrlem2 5380  addcnsr 5407  mulcnsr 5408  axaddopr 5419  axmulopr 5420  axaddrcl 5426  axmulrcl 5428  axrnegex 5437  axrrecex 5438  axcnre 5440  pre-axltadd 5443  pre-axmulgt0 5444  cnegexlem1 5499  cnegex 5502  addcani 5505  addcan 5506  negeui 5509  negeq 5513  subcl 5521  subaddi 5525  subadd 5529  negsub 5536  ine0 5588  1re 5589  mulneg1 5605  mul2neg 5608  negdi 5609  ltadd2i 5744  addge0i 5753  add20i 5756  mulge0i 5761  msqge0i 5768  ltadd1 5777  leadd1 5779  ltsubadd 5781  lesubadd 5783  lt2add 5797  le2add 5798  addgt0 5801  addgegt0 5802  addge0 5804  lesub0 5832  mulge0 5833  mulge0OLD 5834  recextlem2 5839  recex 5840  mulcani 5842  mulcant2i 5843  mul0ori 5846  mul0or 5848  receui 5853  divmuli 5857  divmulzi 5858  divmul 5859  divclzi 5863  divcl 5864  divcan1zi 5870  divcan2zi 5871  divcan1 5872  recne0zi 5877  recne0 5878  recid 5881  divreczi 5884  divrec 5885  divdirzi 5895  divdir 5896  divcan3 5901  div11 5904  recrec 5915  rec11ii 5916  rec11i 5917  redivcli 5938  redivclzi 5939  redivcl 5940  eqnegi 5944  ltmul1i 5962  ltdiv1i 5964  prodgt0 5966  prodge0 5968  ltmul1 5970  lemul1a 5981  lemul1aOLD 5982  ltdiv1 5993  ltdiv1OLD 5994  ltmuldiv 6007  ltmuldivOLD 6008  ltreci 6024  lt2msqi 6026  ltrec 6029  lerec 6030  nnaddcl 6085  nnmulcl 6086  nnsub 6103  nndiv 6105  2times 6150  nn0addcl 6288  nn0mulcli 6290  nn0mulcl 6291  nnnn0addcl 6293  nn0sub 6329  zdiv 6356  zq 6399  qreccl 6412  modval 6460  icoshftf1olem 6537  icoun 6540  snunioo 6542  uzaddcl 6576  fzrevral 6650  fzshftral 6653  fsequb 6654  cardfz 6671  seq1rn2 6686  ser1f 6693  shftfval 6707  seqzfveq 6749  seqzrn2 6751  dfseq0 6758  expp1 6769  expcllem 6770  1exp 6779  expeq0 6780  expne0i 6782  expgt0 6783  expge0 6785  expgt1 6786  expge1 6787  mulexp 6788  exprec 6789  exprecOLD 6790  expadd 6791  expmul 6792  expcan 6798  expwordi 6800  expmwordi 6803  exple1 6804  sqlecan 6838  binom2 6847  bernneq 6849  bernneqOLD 6850  expnbnd 6852  discrlem2 6858  discrlem 6860  nn0opth2 6869  sqrlem21 6894  sqrmuli 6906  sqr2irrlem5 6929  crui 6938  cru 6939  crne0i 6940  creur 6943  creui 6944  replim 6962  reim0b 6976  readd 7006  imadd 7009  cjadd 7013  cjmul 7014  cjexp 7018  abs00i 7044  absmul 7060  absdiv 7062  absexp 7070  cjdiv 7092  abssub 7097  abstri 7101  abs1mi 7107  recan 7108  abs3lem 7110  ser1absdiflem 7132  facdiv 7145  faclbnd3 7150  faclbnd4lem1 7151  faclbnd4lem2 7152  faclbnd4lem3 7153  faclbnd4lem4 7154  faclbnd6 7157  bcval 7161  bcpasc2 7171  bcpasci 7172  bcpasc 7173  bccl2 7174  clim 7180  fsump1slem 7215  fsumcllem 7217  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  csbfsumlem 7229  fsumcom 7231  fsumrev 7232  fsumshft 7234  fsummulc1 7236  fsumconst 7241  fsumcmp 7243  fsumcmpndx2 7245  fsumabs 7246  binomlem1 7269  binomlem2 7270  binomlem3 7271  binomlem4 7272  binomlem6 7274  binomi 7275  bcxmaslem1 7277  bcxmas 7279  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  infcvgi 7428  expcnvlem3 7433  explecnv 7438  geoseri 7439  geolimilem 7440  geolim 7442  geolim1i 7443  geolim1 7444  cvgratlem1ALT 7452  cvgratlem2ALT 7453  cvgratlem1 7455  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag 7463  fsum0diag2 7464  fsum0diag4 7466  mulc1cncf 7484  ivthlem6 7491  ivthlem7 7492  efcltlem1 7509  dfef2i 7512  ef0lem 7515  efcl 7517  efcvg 7519  eftval 7521  erelem2 7525  erelem3 7526  erelem6 7529  efaddlem6 7548  efaddlem24 7566  efaddlem26 7568  efaddlem27 7569  efadd 7572  efexp 7577  ef1tllem 7586  ef01tlubi 7591  absef01tlubi 7593  eirr 7599  ef4p 7608  eflegeolem2 7622  eflegeo 7624  efm1legeo 7626  efcnlem4 7630  sinval 7637  cosval 7638  sinadd 7661  cosadd 7662  absef 7692  demoivre 7695  acdc2lem1 7700  acdc5lem1 7703  infpnlem2 7719  ruclem4 7725  ruclem32 7753  infmap2 7793  retopbas 7865  meteq0 8022  mettri2 8023  mettri4 8024  elbl 8048  blelrn 8058  blss 8063  ssblex 8066  blnei 8089  metcnp 8098  blssioo 8124  tgioolem 8125  lmbr 8139  fsumcnlem 8200  bcthlem15 8224  bcthlem17 8226  isgrp 8254  grpass 8260  grpidinvlem1 8261  grpidinvlem3 8263  grpidinvlem4 8264  grpidinv 8265  grpideu 8266  grpsn 8273  grpidinv2 8277  grprcan 8280  grpinvval 8284  grpinv 8286  grpinvid1 8289  grplcan 8292  isgrp2i 8293  gxnn0neg 8319  gxnn0suc 8320  gxcl 8321  gxcom 8325  gxinv 8326  gxid 8329  gxnn0add 8330  gxnn0mul 8333  grplactval 8338  grplactf1o 8339  ablcom 8344  gxdi 8355  issubgilem 8363  ablsn 8366  ghgrpilem1 8374  ghgrpilem3 8376  ghgrpilem4 8377  ghgrpi 8378  ringid 8386  ringideu 8387  ringdi 8388  ringdir 8389  ringass 8390  cnring 8404  ringsn 8405  vcid 8417  vcdi 8418  vcdir 8419  vcass 8420  nvmul0or 8519  nvs 8537  nvtri 8545  sm1cnilem 8601  ipval 8607  lnolin 8669  bloval 8696  nmlno0 8710  blocnilem 8719  phpar2 8738  phpar 8739  ipdiri 8745  ipassi 8757  siilem1 8767  siii 8769  sii 8770  ip2eqi 8773  ajfun 8777  minveclem13 8817  minvecex 8838  minveceu 8843  minvecdist 8845  minveclem39 8847  htthlem2 8883  sincolem 8932  sineq0re 8985  efgh 8990  efghgrpilem 8991  efif 8993  efifo 9001  efif1lem6 9007  efif1 9009  shftefif1olem 9013  eff1i 9016  effoi 9017  hvsubval 9161  hvmul0or 9169  hvsubsub4 9202  hvaddcani 9207  hvnegdi 9209  hvsubeq0 9210  hvaddcan 9212  hvsubadd 9220  hial0 9244  hial02 9245  hial2eq 9248  normlem6 9257  normlem9at 9263  normsub0 9279  norm-ii 9281  norm-iii 9283  normsub 9286  normpyth 9288  norm3dif 9293  norm3lemt 9295  norm3adifi 9296  normpar 9298  polid 9302  bcs 9324  hlimi 9332  hlim2 9336  shaddcl 9361  shaddclOLD 9362  shmulcl 9363  shmulclOLD 9364  hsn0elch 9396  ocsh 9432  ocorth 9440  ocin 9445  occllem2 9450  occllem7 9455  occllem8 9456  projlem1 9462  projlem7 9468  projlem17 9478  projlem20 9481  projlem22 9483  projlem26 9487  projlem28 9489  pjthlem13 9507  pjthlem14 9508  pjtheui 9511  omlsii 9521  pjoc1i 9540  shsel3 9555  shscli 9557  shscl 9558  choc0 9566  shslej 9626  shlub 9630  chlejb1 9711  chnle 9713  chjass 9732  ledi 9739  h1deoi 9748  h1de2i 9752  elspansn 9765  elspansn2 9766  spanunsni 9778  h1datomi 9780  pjoml6i 9808  cmbr3 9827  pjoml3 9831  osumlem5 9860  osumlem8 9863  osum 9866  spansncvi 9875  pjadji 9908  pjaddi 9909  pjsubi 9911  pjmuli 9912  pjcjt2 9915  hosubcl 9979  hoaddcom 9980  hoaddass 9988  hocsubdir 9991  ho0sub 10003  honegsub 10005  adjsym 10039  eigrei 10040  eigre 10041  eigposi 10042  eigorthi 10043  eigorth 10044  cnopc 10117  lnopl 10118  unop 10119  hmop 10126  cnfnc 10134  lnfnl 10135  adj1 10137  adjvalval 10141  braval 10147  kbval 10156  eleigvec 10161  hoddi 10194  lnopeq0lem2 10210  lnopunii 10216  lnophmi 10222  nmcopexlem4 10233  nmcopexi 10236  nmcfnexlem4 10262  nmcfnexi 10265  riesz3i 10274  riesz4i 10275  cnlnadjlem4 10282  cnlnadjlem5 10283  cnlnadji 10288  nmopadjlei 10300  nmopcoi 10307  cnvbraval 10323  leopg 10335  hmopidmchi 10359  pjclem3 10406  hstel2 10427  stj 10443  mdbr 10502  dmdbr 10507  mdsl0 10518  chcv1 10563  chjatom 10565  cvexch 10582  atcvat4i 10606  sumdmdlem 10627  cdjreui 10641  cdj1i 10642  cdj3lem1 10643  cdj3lem2 10644  cdj3lem2b 10646  cdj3lem3b 10649  cdj3i 10650  ghomgrpilem1 10670  ghomlin 10678  elgiso 10683  cayleylem2 10695  cayleythlem 10698  labss1 10837  labss2 10839  jidd 10840  midd 10841  nfwval 10874  opidon 10898  exidu1 10902  cmpidelt 10906  smgrpass2 10914  isppm 10917  mndass2 10932  rngmgmbs4 10945  ununr 10955  uznzr 10967  hmph 11030  altretop 11144  iintlem1 11155  iintlem2 11156  1ded 11192  domcmpd 11200  codcmpd 11201  cmpasso 11227  cmpida 11228  ismonb2 11267  cmpmon 11270  icmpmon 11271  idmon 11272  isepib 11275  cinvlem3 11284  subtopmet 11506  reconn 11512  ivthALT 11515  rnelfm 11699  fmfnfm 11704  flimff 11707  fcluscnplem 11729  fcluscnp 11730  fclusff 11735  gagrpid 11780  gaass 11781  gacan 11782  add20 11858  divexp 11859  eluzadd 11860  eluzsub 11861  fzfi 11864  sdclem1 11875  sdclem2 11876  sdc 11877  fsum00 11883  fsumlt 11884  fsumltisumi 11886  fsumltisum 11887  fsumleisumi 11889  fsumleisum 11890  iserzshft2 11892  isumshft2 11893  fsumlt1 11894  trirn 11897  metsstop 11909  mettrifi 11912  geomcau 11914  metdcn 11918  lincmb01icc 11943  sub2cncf 11947  txcnoprab 11981  sstotbnd 11992  totbndss 11993  isbnd3 11997  blbnd 11999  totbndbnd 12000  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem16 12026  heiborlem23 12033  heiborlem25 12035  heiborlem26 12036  heiborlem28 12038  heiborlem29 12039  heiborlem30 12040  heiborlem32 12042  heiborlem35 12045  bfplem5 12058  bfplem8 12061  bfplem9 12062  bfplem11 12064  recms 12066  rrnval 12069  iccbnd 12082  phtpyfval 12088  phtpycom 12092  phtpycolem1 12093  phtpycolem2 12094  phtpycolem3 12095  phtpycolem4 12096  phtpyco 12098  phtpcval 12100  isphtpc 12101

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279  df-opr 4023

Copyright terms: Public domain