Theorem eqcomi 1526

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 1524	. 2 |- (A = B <-> B = A)
3	1, 2	mpbi 196	1 |- B = A

Syntax hints:   = wceq 997

This theorem is referenced by:  eqtr2i 1543  eqtr3i 1544  eqtr4i 1545  3eqtr2ri 1549  syl5eqr 1568  syl5reqr 1569  syl6eqr 1572  syl6reqr 1573  eqeltrri 1592  eleqtrri 1594  syl5eqelr 1600  syl6eleqr 1606  abid2 1627  eqsstr3i 2143  sseqtr4i 2145  syl5ssr 2157  syl6ssr 2159  inrab2 2323  elsncg 2482  eqbrtrri 2691  breqtrri 2695  syl6breqr 2710  csbopabg 2733  pwin 2881  orduniss2 3147  limon 3151  unizlim 3170  orduninsuc 3171  tfis 3184  cnvresid 3626  fores 3738  fo1st 4149  fo2nd 4150  om0r 4232  fiprlemOLD 4494  fiprOLD 4496  sbthlem5 4514  fodomr 4546  phplem4 4576  supub 4640  suplub 4641  rankpw 4746  rankval4 4764  cardnum 4954  negsubi 5446  eqnegi 5862  halfposi 5964  zeo 6284  seq0seqz 6631  sqrlem11 6773  sqr4 6807  sqr9 6808  sqr2irrlem4 6817  cjmuli 6879  imi 6915  fac2 7027  fac3 7028  faclbnd4lem1 7038  fsummulc1 7123  binomi 7162  iserzshfti 7234  isumshft2i 7295  isumnn0nnai 7298  isumspliti 7306  arisumi 7316  geolimilem 7325  isupivthi 7380  efcl 7402  eirrlem1 7479  eirrlem5 7483  efsepi 7487  ef4pi 7490  cos2tsin 7555  cos2bnd 7567  sin01gt0 7568  infxpidmlem7 7650  subtop 7733  retps 7743  neif 7800  qdensere 7836  idcn 7851  cnpco 7854  methausi 7966  xplmi 8058  xplm 8060  xpcn 8061  bcthlem5 8088  bcthlem12 8095  isgrpi 8127  grpfo 8128  0ngrp 8140  isgrp2i 8160  cnid 8211  ringsn 8247  nvvc 8318  nvdm 8373  nvtri 8382  nmcn3 8425  abscncfALT 8428  sspval 8466  cnbn 8612  ubthlem6 8618  ubthlem8 8620  minvecdist 8669  cos2pi 8768  sincos6thpi 8794  eff1o 8831  loge 8850  pilog 8851  1p1e2 8870  hvsubcan2i 9014  normlem1 9059  normlem2 9060  bcseqi 9069  normpar2i 9106  hhnv 9115  hhshsslem1 9220  hhshsslem2 9221  hhssvs 9225  ococi 9330  pjpj0i 9338  shscli 9364  shlubi 9429  qlax1i 9651  qlaxr1i 9656  osumi 9669  hosd1i 9831  pjhmopidm 10193  pjin1i 10204  hatomistici 10373  symgoprab 10487  symgidi 10492  cayleylem3 10496  fine 10533  abfi 10534  mapdiscn 10605  cmphmp 10615  hmeobc 10636  fgsb 10663  rcfpfillem3 10673  sfvlimOLD 10685  usinuniop 10703  clicls 10704  isalg 10735  1alg 10736  algi 10742  dedi 10752  1ded 10753  cati 10770  0alg 10771  1cat 10774  dmo 10791  cmpmorp 10794  mrdmcd 10804  homib 10806  cmphmia 10808  cmphmib 10809  iri 10810  ismona 10819  idmon 10827  isepia 10829

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-cleq 1515

Copyright terms: Public domain