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  6742  1p1e2  7791  1e2m1  7793  2p1e3  7801  3p1e4  7803  4p1e5  7804  5p1e6  7805  6p1e7  7806  7p1e8  7807  8p1e9  7808  9p1e10  7809  0mnnnnn0  7970  zeo  8099  num0u  8132  numsucc  8149  1e0p1  8151  nummac  8155  6p5lem  8172  5t5e25  8199  6t6e36  8204  8t6e48  8215  decbin3  8228  ige3m2fz  8663  fseq1p1m1  8706  fz0tp  8731  1fv  8746  fzo0to42pr  8826  fzosplitprm1  8840  expnegap0  8897  imi  9108  bdceqir  9279  bj-ssom  9370