Theorem eqcomi 1471

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

Syntax hints:   = wceq 953

This theorem is referenced by:  eqtr2 1488  eqtr3 1489  eqtr4 1490  3eqtr2r 1494  syl5eqr 1513  syl5reqr 1514  syl6eqr 1517  syl6reqr 1518  eqeltrr 1537  eleqtrr 1539  syl5eqelr 1545  syl6eleqr 1551  abid2 1572  eqsstr3 2082  sseqtr4 2084  syl5ssr 2096  syl6ssr 2098  inrab2 2262  elsncg 2420  eqbrtrr 2626  breqtrr 2630  syl6breqr 2645  csbopabg 2668  pwin 2814  orduniss2 3080  limon 3084  unizlim 3103  orduninsuc 3104  tfis 3117  cnvresid 3555  fores 3666  fo1st 4075  fo2nd 4076  om0r 4158  sbthlem5 4431  fodomr 4463  phplem4 4491  supub 4554  suplub 4555  rankpw 4656  rankval4 4674  cardnum 4861  negsub 5353  eqneg 5760  halfpos 5852  zeot 6146  seq0seqz 6474  sqrlem11 6613  sqr4 6647  sqr9 6648  sqr2irrlem4 6657  cjmul 6724  imi 6760  fac2 6874  fac3 6875  faclbnd4lem1 6885  fsummulc1 6971  binom 7010  iserzshft 7080  isumshft2 7140  isumnn0nna 7143  isumsplit 7151  fnsmnt 7161  geolimilem 7170  isupivth 7225  efclt 7254  eirrlem1 7330  eirrlem5 7334  efsep 7337  ef4p 7340  cos2bnd 7417  sin01gt0 7418  infxpidmlem7 7501  subbas2 7587  subtop 7588  retps 7600  neif 7656  qdensere 7691  idcn 7705  cnpco 7708  methausi 7820  xplmi 7907  xplm 7909  xpcn 7910  bcthlem5 7937  bcthlem12 7944  isgrpi 7976  grpfo 7977  0ngrp 7989  isgrp2i 8011  cnid 8064  ringsn 8100  nvvc 8174  nvtri 8237  abscncfALT 8278  sspval 8316  cnbn 8459  ubthlem6 8465  ubthlem8 8467  minvecdist 8516  cos2pi 8604  sincos6thpi 8628  eff1o 8670  loge 8689  pilog 8690  logeOLD 8708  1p1e2 8726  hvsubcan2 8852  normlem1 8897  normlem2 8898  bcseq 8907  normpar2 8944  hhnv 8953  hhshsslem1 9057  hhshsslem2 9058  hhssvs 9061  ococ 9162  pjpj0 9170  shscl 9196  shlub 9261  qlax1 9485  qlaxr1 9490  osum 9503  hosd1 9665  pjhmopidm 10020  pjin1 10030  hatomistic 10197  symgoprab 10307  symgidiOLD 10312  symgidi 10314  cayleylem3 10318  fine 10348  abfi 10349  mapdiscn 10398  cmphmp 10408  isfil 10433  fillsb 10435  fgsb 10444  clicls 10466  isalg 10497  1alg 10498  algi 10504  dedi 10514  1ded 10515  cati 10532  0alg 10533  1cat 10536  dmo 10553  cmpmorp 10556  mrdmcd 10566  homib 10568  cmphmia 10570  cmphmib 10571  iri 10572  ismona 10579  idmon 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain