Theorem eqcomi 1482

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

Syntax hints:   = wceq 958

This theorem is referenced by:  eqtr2 1499  eqtr3 1500  eqtr4 1501  3eqtr2r 1505  syl5eqr 1524  syl5reqr 1525  syl6eqr 1528  syl6reqr 1529  eqeltrr 1548  eleqtrr 1550  syl5eqelr 1556  syl6eleqr 1562  abid2 1583  eqsstr3 2096  sseqtr4 2098  syl5ssr 2110  syl6ssr 2112  inrab2 2276  elsncg 2435  eqbrtrr 2642  breqtrr 2646  syl6breqr 2661  csbopabg 2684  pwin 2832  orduniss2 3097  limon 3101  unizlim 3120  orduninsuc 3121  tfis 3134  cnvresid 3576  fores 3688  fo1st 4098  fo2nd 4099  om0r 4181  sbthlem5 4458  fodomr 4490  phplem4 4518  supub 4596  suplub 4597  rankpw 4701  rankval4 4719  cardnum 4907  negsub 5400  eqneg 5813  halfpos 5913  zeot 6208  seq0seqz 6550  sqrlem11 6691  sqr4 6725  sqr9 6726  sqr2irrlem4 6735  cjmul 6796  imi 6832  fac2 6944  fac3 6945  faclbnd4lem1 6955  fsummulc1 7040  binom 7079  iserzshft 7151  isumshft2 7212  isumnn0nna 7215  isumsplit 7223  fnsmnt 7233  geolimilem 7242  isupivth 7297  efclt 7319  eirrlem1 7396  eirrlem5 7400  efsep 7403  ef4p 7406  cos2tsint 7471  cos2bnd 7483  sin01gt0 7484  infxpidmlem7 7566  subtop 7650  retps 7662  neif 7719  qdensere 7755  idcn 7770  cnpco 7773  methausi 7885  xplmi 7977  xplm 7979  xpcn 7980  bcthlem5 8007  bcthlem12 8014  isgrpi 8046  grpfo 8047  0ngrp 8059  isgrp2i 8079  cnid 8130  ringsn 8166  nvvc 8237  nvdm 8292  nvtri 8301  nmcn3 8344  abscncfALT 8347  sspval 8385  cnbn 8531  ubthlem6 8537  ubthlem8 8539  minvecdist 8588  cos2pi 8687  sincos6thpi 8713  eff1o 8750  loge 8769  pilog 8770  1p1e2 8789  hvsubcan2 8933  normlem1 8978  normlem2 8979  bcseq 8988  normpar2 9025  hhnv 9034  hhshsslem1 9139  hhshsslem2 9140  hhssvs 9144  ococ 9249  pjpj0 9257  shscl 9283  shlub 9348  qlax1 9570  qlaxr1 9575  osum 9588  hosd1 9750  pjhmopidm 10112  pjin1 10123  hatomistic 10292  symgoprab 10405  symgidi 10410  cayleylem3 10414  fine 10450  abfi 10451  mapdiscn 10505  cmphmp 10515  hmeobc 10536  fgsb 10563  rcfpfillem3 10573  sfvlimOLD 10585  clicls 10601  isalg 10632  1alg 10633  algi 10639  dedi 10649  1ded 10650  cati 10667  0alg 10668  1cat 10671  dmo 10688  cmpmorp 10691  mrdmcd 10701  homib 10703  cmphmia 10705  cmphmib 10706  iri 10707  ismona 10716  idmon 10724  isepia 10726

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472

Copyright terms: Public domain