Theorem eqcomi 1516

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

Syntax hints:   = wceq 988

This theorem is referenced by:  eqtr2i 1533  eqtr3i 1534  eqtr4i 1535  3eqtr2ri 1539  syl5eqr 1558  syl5reqr 1559  syl6eqr 1562  syl6reqr 1563  eqeltrri 1582  eleqtrri 1584  syl5eqelr 1590  syl6eleqr 1596  abid2 1617  eqsstr3i 2136  sseqtr4i 2138  syl5ssr 2150  syl6ssr 2152  inrab2 2316  elsncg 2475  eqbrtrri 2686  breqtrri 2690  syl6breqr 2705  csbopabg 2729  pwin 2879  orduniss2 3145  limon 3149  unizlim 3168  orduninsuc 3169  tfis 3182  cnvresid 3644  fores 3757  fo1st 4169  fo2nd 4170  om0r 4258  sbthlem5 4538  fodomr 4570  phplem4 4600  supub 4664  suplub 4665  rankpw 4770  rankval4 4788  cardnum 4978  negsubi 5470  eqnegi 5888  halfposi 5991  zeo 6312  seq0seqz 6665  sqrlem11 6806  sqr4 6840  sqr9 6841  sqr2irrlem4 6850  cjmuli 6912  imi 6948  fac2 7060  fac3 7061  faclbnd4lem1 7071  fsummulc1 7156  binomi 7195  iserzshfti 7267  isumshft2i 7328  isumnn0nnai 7331  isumspliti 7339  arisumi 7349  geolimilem 7358  isupivthi 7413  efcl 7435  eirrlem1 7512  eirrlem5 7516  efsepi 7520  ef4pi 7523  cos2tsin 7588  cos2bnd 7600  sin01gt0 7601  infxpidmlem7 7683  subtop 7768  retps 7778  neif 7835  qdensere 7871  idcn 7886  cnpco 7889  methausi 8001  xplmi 8093  xplm 8095  xpcn 8096  bcthlem5 8123  bcthlem12 8130  isgrpi 8162  grpfo 8163  0ngrp 8175  isgrp2i 8195  cnid 8246  ringsn 8282  nvvc 8353  nvdm 8408  nvtri 8417  nmcn3 8460  abscncfALT 8463  sspval 8501  cnbn 8647  ubthlem6 8653  ubthlem8 8655  minvecdist 8704  cos2pi 8803  sincos6thpi 8830  eff1o 8867  loge 8886  pilog 8887  1p1e2 8906  hvsubcan2i 9050  normlem1 9096  normlem2 9097  bcseqi 9106  normpar2i 9143  hhnv 9152  hhshsslem1 9257  hhshsslem2 9258  hhssvs 9262  ococi 9367  pjpj0i 9375  shscli 9401  shlubi 9466  qlax1i 9688  qlaxr1i 9693  osumi 9706  hosd1i 9868  pjhmopidm 10227  pjin1i 10238  hatomistici 10407  symgoprab 10523  symgidi 10528  cayleylem3 10532  fine 10570  abfi 10571  mapdiscn 10647  cmphmp 10657  hmeobc 10678  subspemp 10692  fgsb 10708  rcfpfillem3 10718  sfvlimOLD 10730  usinuniop 10753  singempcon 10755  clicls 10757  isalg 10788  1alg 10789  algi 10795  dedi 10805  1ded 10806  cati 10823  0alg 10824  1cat 10827  dmo 10844  cmpmorp 10847  mrdmcd 10857  homib 10859  cmphmia 10861  cmphmib 10862  iri 10863  ismona 10872  idmon 10880  isepia 10882  cinvlem2 10891

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1505

Copyright terms: Public domain