Theorem eqcomi 2044

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

Hypothesis

Ref	Expression
eqcomi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqcomi	⊢ 𝐵 = 𝐴

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ 𝐴 = 𝐵
2		eqcom 2042	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 133	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1243

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 1336  ax-gen 1338  ax-ext 2022

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

This theorem is referenced by:  eqtr2i  2061  eqtr3i  2062  eqtr4i  2063  syl5eqr  2086  syl5reqr  2087  syl6eqr  2090  syl6reqr  2091  eqeltrri  2111  eleqtrri  2113  syl5eqelr  2125  syl6eleqr  2131  abid2  2158  abid2f  2202  eqnetrri  2230  neeqtrri  2234  eqsstr3i  2976  sseqtr4i  2978  syl5eqssr  2990  syl6sseqr  2992  difdif2ss  3194  inrab2  3210  dfopg  3547  opid  3567  eqbrtrri  3785  breqtrri  3789  syl6breqr  3804  pwin  4019  limon  4239  tfis  4306  dfdm2  4852  cnvresid  4973  fores  5115  funcoeqres  5157  f1oprg  5168  fmptpr  5355  fsnunres  5364  riotaprop  5491  fo1st  5784  fo2nd  5785  phplem4  6318  snnen2og  6322  phplem4on  6329  caucvgsrlembound  6878  ax0id  6952  1p1e2  8033  1e2m1  8035  2p1e3  8043  3p1e4  8045  4p1e5  8046  5p1e6  8047  6p1e7  8048  7p1e8  8049  8p1e9  8050  9p1e10  8051  div4p1lem1div2  8177  0mnnnnn0  8214  zeo  8343  num0u  8376  numsucc  8393  1e0p1  8395  nummac  8399  6p5lem  8416  5t5e25  8443  6t6e36  8448  8t6e48  8459  decbin3  8472  ige3m2fz  8913  fseq1p1m1  8956  fz0tp  8981  1fv  8996  fzo0to42pr  9076  fzosplitprm1  9090  expnegap0  9263  imi  9500  ex-ceil  9896  bdceqir  9964  bj-ssom  10060