Theorem eqcomi 2041

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

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 2039	. 2 ⊢ (A = B ↔ B = A)
3	1, 2	mpbi 133	1 ⊢ B = A

Syntax hints:   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030

This theorem is referenced by:  eqtr2i  2058  eqtr3i  2059  eqtr4i  2060  syl5eqr  2083  syl5reqr  2084  syl6eqr  2087  syl6reqr  2088  eqeltrri  2108  eleqtrri  2110  syl5eqelr  2122  syl6eleqr  2128  abid2  2155  abid2f  2199  eqnetrri  2224  neeqtrri  2228  eqsstr3i  2970  sseqtr4i  2972  syl5eqssr  2984  syl6sseqr  2986  difdif2ss  3188  inrab2  3204  dfopg  3538  opid  3558  eqbrtrri  3776  breqtrri  3780  syl6breqr  3795  pwin  4010  limon  4204  tfis  4249  dfdm2  4795  cnvresid  4916  fores  5058  funcoeqres  5100  f1oprg  5111  fmptpr  5298  fsnunres  5307  riotaprop  5434  fo1st  5726  fo2nd  5727  ax0id  6762  1p1e2  7811  1e2m1  7813  2p1e3  7821  3p1e4  7823  4p1e5  7824  5p1e6  7825  6p1e7  7826  7p1e8  7827  8p1e9  7828  9p1e10  7829  0mnnnnn0  7990  zeo  8119  num0u  8152  numsucc  8169  1e0p1  8171  nummac  8175  6p5lem  8192  5t5e25  8219  6t6e36  8224  8t6e48  8235  decbin3  8248  ige3m2fz  8683  fseq1p1m1  8726  fz0tp  8751  1fv  8766  fzo0to42pr  8846  fzosplitprm1  8860  expnegap0  8917  imi  9128  bdceqir  9299  bj-ssom  9395