Theorem eqcomi 1477

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

Syntax hints:   = wceq 955

This theorem is referenced by:  eqtr2 1494  eqtr3 1495  eqtr4 1496  3eqtr2r 1500  syl5eqr 1519  syl5reqr 1520  syl6eqr 1523  syl6reqr 1524  eqeltrr 1543  eleqtrr 1545  syl5eqelr 1551  syl6eleqr 1557  abid2 1578  eqsstr3 2089  sseqtr4 2091  syl5ssr 2103  syl6ssr 2105  inrab2 2269  elsncg 2427  eqbrtrr 2632  breqtrr 2636  syl6breqr 2651  csbopabg 2674  pwin 2821  orduniss2 3086  limon 3090  unizlim 3109  orduninsuc 3110  tfis 3123  cnvresid 3565  fores 3676  fo1st 4084  fo2nd 4085  om0r 4167  sbthlem5 4440  fodomr 4472  phplem4 4500  supub 4563  suplub 4564  rankpw 4667  rankval4 4685  cardnum 4872  negsub 5364  eqneg 5770  halfpos 5862  zeot 6156  seq0seqz 6487  sqrlem11 6628  sqr4 6662  sqr9 6663  sqr2irrlem4 6672  cjmul 6739  imi 6775  fac2 6889  fac3 6890  faclbnd4lem1 6900  fsummulc1 6986  binom 7025  iserzshft 7097  isumshft2 7157  isumnn0nna 7160  isumsplit 7168  fnsmnt 7178  geolimilem 7187  isupivth 7242  efclt 7271  eirrlem1 7347  eirrlem5 7351  efsep 7354  ef4p 7357  cos2bnd 7434  sin01gt0 7435  infxpidmlem7 7518  subbas2 7605  subtop 7606  retps 7618  neif 7675  qdensere 7711  idcn 7726  cnpco 7729  methausi 7843  xplmi 7935  xplm 7937  xpcn 7938  bcthlem5 7965  bcthlem12 7972  isgrpi 8004  grpfo 8005  0ngrp 8017  isgrp2i 8038  cnid 8091  ringsn 8127  nvvc 8198  nvdm 8253  nvtri 8262  abscncfALT 8306  sspval 8344  cnbn 8487  ubthlem6 8493  ubthlem8 8495  minvecdist 8544  cos2pi 8639  sincos6thpi 8663  eff1o 8703  loge 8722  pilog 8723  1p1e2 8742  hvsubcan2 8886  normlem1 8931  normlem2 8932  bcseq 8941  normpar2 8978  hhnv 8987  hhshsslem1 9092  hhshsslem2 9093  hhssvs 9097  ococ 9202  pjpj0 9210  shscl 9236  shlub 9301  qlax1 9525  qlaxr1 9530  osum 9543  hosd1 9705  pjhmopidm 10066  pjin1 10076  hatomistic 10245  symgoprab 10358  symgidi 10363  cayleylem3 10367  fine 10406  abfi 10407  mapdiscn 10457  cmphmp 10467  isfil 10492  fillsb 10494  fgsb 10503  rcfpfillem3 10513  sfvlim 10522  clicls 10538  isalg 10569  1alg 10570  algi 10576  dedi 10586  1ded 10587  cati 10604  0alg 10605  1cat 10608  dmo 10625  cmpmorp 10628  mrdmcd 10638  homib 10640  cmphmia 10642  cmphmib 10643  iri 10644  ismona 10651  idmon 10660

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974  ax-ext 1458

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

Copyright terms: Public domain