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  6722  1p1e2  7771  1e2m1  7773  2p1e3  7781  3p1e4  7783  4p1e5  7784  5p1e6  7785  6p1e7  7786  7p1e8  7787  8p1e9  7788  9p1e10  7789  0mnnnnn0  7950  zeo  8079  num0u  8112  numsucc  8129  1e0p1  8131  nummac  8135  6p5lem  8152  5t5e25  8179  6t6e36  8184  8t6e48  8195  decbin3  8208  ige3m2fz  8643  fseq1p1m1  8686  fz0tp  8711  1fv  8726  fzo0to42pr  8806  fzosplitprm1  8820  expnegap0  8877  imi  9088  bdceqir  9233  bj-ssom  9324