Theorem eqcomi 2026

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

Syntax hints:   = wceq 1228

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 1316  ax-gen 1318  ax-ext 2004

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

This theorem is referenced by:  eqtr2i  2043  eqtr3i  2044  eqtr4i  2045  syl5eqr  2068  syl5reqr  2069  syl6eqr  2072  syl6reqr  2073  eqeltrri  2093  eleqtrri  2095  syl5eqelr  2107  syl6eleqr  2113  abid2  2140  abid2f  2184  eqnetrri  2208  neeqtrri  2212  eqsstr3i  2953  sseqtr4i  2955  syl5eqssr  2967  syl6sseqr  2969  difdif2ss  3171  inrab2  3187  dfopg  3521  opid  3541  eqbrtrri  3759  breqtrri  3763  syl6breqr  3778  pwin  3993  limon  4188  tfis  4233  dfdm2  4779  cnvresid  4899  fores  5040  funcoeqres  5082  f1oprg  5093  fmptpr  5280  fsnunres  5289  riotaprop  5415  fo1st  5707  fo2nd  5708  ax0id  6572  bdceqir  7071  bj-ssom  7158