Theorem eqcomi 1888

Description: Inference from commutative law for class equality.

Hypothesis

Ref	Expression
eqcomi.1	|- A = B

Assertion

Ref	Expression
eqcomi	|- B = A

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 |- A = B
2		eqcom 1886	. 2 |- (A = B <-> B = A)
3	1, 2	mpbi 206	1 |- B = A

Syntax hints:   = wceq 1298

This theorem is referenced by:  eqtr2i 1909  eqtr3i 1910  eqtr4i 1911  3eqtr2riOLD 1917  syl5eqr 1942  syl5reqr 1943  syl6eqr 1946  syl6reqr 1947  eqeltrri 1968  eleqtrri 1970  syl5eqelr 1976  syl6eleqr 1982  abid2 2011  abid2f 2012  eqsstr3i 2648  sseqtr4i 2650  syl5ssr 2662  syl6ssr 2664  inrab2 2867  elsncgOLD 3064  hbeqel 3195  eqbrtrri 3358  breqtrri 3362  syl6breqr 3377  csbopabg 3409  pwin 3576  unizlim 3786  reusn 3818  orduniss2 3913  limon 3917  orduninsuc 3925  tfis 3938  dfdm2 4421  cnvresid 4488  fores 4627  fvopab6 4757  fo1st 5032  fo2nd 5033  om0r 5221  sbthlem5 5514  fodomr 5547  phplem4 5605  supub 5670  suplub 5671  rankpw 5795  rankval4 5813  omsubsuc 5877  cardnum 6037  negsubi 6538  negsubiOLD 6539  eqnegi 6982  halfposi 7087  addltmul 7229  zeo 7411  seq0seqz 7785  sqrlem11 7933  sqr4 7967  sqr9 7968  sqr2irrlem4 7977  cjmuli 8039  imi 8075  fac2 8189  fac3 8190  faclbnd4lem1 8200  fsummulc1 8293  binomi 8332  iserzshfti 8404  isumshft2i 8466  isumnn0nnai 8469  isumspliti 8477  arisumi 8487  geolimilem 8497  isupivthi 8552  efcl 8574  eirrlem1 8651  eirrlem5 8655  efsepi 8661  ef4pi 8664  cos2tsin 8729  cos2bnd 8741  sin01gt0 8742  infxpidmlem7 8827  subbas2 8915  subtop 8916  retps 8928  neif 8991  qdensere 9027  idcn 9042  cnpco 9046  methausi 9159  xplmi 9251  xplm 9253  xpcn 9254  bcthlem5 9281  bcthlem12 9288  isgrpi 9322  grpfo 9323  0ngrp 9335  grpidvallem 9341  isgrp2i 9360  cnid 9435  ga0 9453  ringsn 9490  nvvc 9566  nvdm 9621  nvtri 9630  vacnlem5 9671  nmcn3 9680  abscncfALT 9683  sspval 9721  cnbn 9871  ubthlem6 9877  ubthlem8 9879  minvecdist 9930  cos2pi 10034  sinq34lt0t 10058  sincos6thpi 10061  eff1o 10102  loge 10121  pilog 10122  1p1e2 10145  dif1en 10172  clicls 10183  clint3 10184  symgoprab 10201  symgidi 10206  istoset 10209  fine 10213  abfi 10215  hmeobc 10239  fbfgfmeq 10315  usinuniop 10341  isass 10363  isexid 10364  ismgm 10367  fora1 10406  on1el3 10412  uznzr 10416  zrdivrng 10418  hvsubcan2i 10563  normlem1 10609  normlem2 10610  bcseqi 10619  normpar2i 10656  hhnv 10665  hhshsslem1 10770  hhshsslem2 10771  hhssvs 10775  ococi 10880  pjpj0i 10888  shscli 10914  shlubi 10979  qlax1i 11203  qlaxr1i 11208  osumi 11221  hosd1i 11385  pjhmopidm 11754  pjin1i 11765  hatomistici 11934  addltmulALT 12018  bnj54OLD 12429  bnj601 13309  cayleylem3 13643  3prm 13780  4nprm 13781  setinds 13844  axbday 14012  boe 14350  cnvref 14371  isunscov 14386  imrescl 14393  fldrels 14449  orkurss 14488  npincppr 14501  repfuntw 14502  2eq3m1 14526  islatalg 14531  toplat 14638  dfdir2 14639  clfsebs 14707  clfsebsr 14709  seqzp2 14716  expm 14725  fnopabco2b 14734  cmprtr 14760  com2i 14765  vecval1b 14794  vecval3b 14795  vecax4 14799  vecax5 14800  mulveczer 14822  mulinvsca 14823  muldisc 14824  svli2 14826  mapdiscnlem 14870  osneisi 14875  elsubops 14877  cmphmp 14878  subspemp 14903  topgele 14910  usptop 14920  fgsb 14921  rcfpfillem3 14930  conttnf 14944  bwt2 14960  clsingemp 14961  singempcon 14965  idtrgrp 14978  invtrgrp 14979  extopgrp 14980  trhom 14983  cntrsetlem 14999  flimfneic 15036  lvsovso3 15040  supnuf 15041  supexr 15043  isalg 15068  1alg 15069  algi 15074  dedi 15084  1ded 15085  dmrngcmp 15098  cati 15102  0alg 15103  1cat 15106  dmo 15123  cmpmorp 15126  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  dualcat2 15133  mrdmcd 15143  homib 15145  cmphmia 15147  cmphmib 15148  iri 15149  ismona 15158  idmon 15166  isepia 15168  cinvlem2 15177  idsubidsup 15205  valtar 15260  isplibg0 15307  isplibg1 15309  isplibg2 15311  isplibg3 15313  isplibg4a 15315  isplibg4b 15317  fictblem 15370  inficlALT 15372  omsubsucOLD 15386  subcls 15424  subntr 15425  cnsubsp2 15427  compsub 15431  uncomp 15433  compfipin0lem 15435  compfipin0 15436  reconnlem1 15446  reconn 15451  retopcon 15452  ivthALT 15454  refssfne 15504  locfindsc 15515  topmtcl 15525  isufil2 15565  ufileu 15573  uffixfr 15575  flimfbas 15601  flimfnfcls 15615  fsumltisumi 15823  csbrni 15832  iiuni 15868  dfii3 15870  piececn 15894  txunii 15910  txcnoprab 15911  cnresoprab 15915  cnopropabco 15917  cnopropabcoc 15918  cnoproprabco 15919  cnoproprabcoc 15920  cnoprab1c 15923  cnoprab2c 15924  txmet 15925  heiborlem11 15965  heiborlem12 15966  heiborlem15 15969  heiborlem16 15970  heiborlem17 15971  heiborlem32 15986  rrncms 16019  reheibor 16025  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  phtpyco 16056  pcocn 16076  pcohtpylem3 16082  pcopt 16084  pcorevlem 16086  pi1bval 16088  sbeqal2i 16357  compne 16417  grpinvfvalNEW 17125

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain