Theorem eqcomi 2181

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 2179	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  eqtr2i  2199  eqtr3i  2200  eqtr4i  2201  eqtr3id  2224  eqtr3di  2225  eqtr4di  2228  eqtr4id  2229  eqeltrri  2251  eleqtrri  2253  eqeltrrid  2265  eleqtrrdi  2271  abid2  2298  abid2f  2345  eqnetrri  2372  neeqtrri  2376  eqsstrri  3188  sseqtrri  3190  eqsstrrid  3202  sseqtrrdi  3204  difdif2ss  3392  inrab2  3408  dfopg  3774  opid  3794  eqbrtrri  4023  breqtrri  4027  breqtrrdi  4042  pwin  4278  limon  4508  tfis  4578  dfdm2  5158  cnvresid  5285  fores  5442  funcoeqres  5487  f1oprg  5500  fnmptfvd  5615  fmptpr  5703  fsnunres  5713  riotaprop  5847  fo1st  6151  fo2nd  6152  fnmpoovd  6209  ixpsnf1o  6729  phplem4  6848  snnen2og  6852  phplem4on  6860  pw1dc0el  6904  ss1o0el1o  6905  sbthlemi5  6953  eldju  7060  casefun  7077  omp1eomlem  7086  exmidfodomrlemim  7193  caucvgsrlembound  7771  ax0id  7855  1p1e2  9012  1e2m1  9014  2p1e3  9028  3p1e4  9030  4p1e5  9031  5p1e6  9032  6p1e7  9033  7p1e8  9034  8p1e9  9035  div4p1lem1div2  9148  0mnnnnn0  9184  zeo  9334  num0u  9370  numsucc  9399  decsucc  9400  1e0p1  9401  nummac  9404  decsubi  9422  decmul1  9423  decmul10add  9428  6p5lem  9429  10m1e9  9455  5t5e25  9462  6t6e36  9467  8t6e48  9478  decbin3  9501  infrenegsupex  9570  ige3m2fz  10022  fseq1p1m1  10067  fz0tp  10095  fz0to4untppr  10097  1fv  10112  fzo0to42pr  10193  fzosplitprm1  10207  expnegap0  10501  sq4e2t8  10590  3dec  10665  fihashen1  10750  pr0hash2ex  10766  imi  10880  infxrnegsupex  11242  zsumdc  11363  fsumadd  11385  hashrabrex  11460  ntrivcvgap  11527  fprodmul  11570  fproddivapf  11610  fprodmodd  11620  efsep  11670  3dvdsdec  11840  3dvds2dec  11841  flodddiv4  11909  lcmneg  12044  ennnfonelem1  12378  nninfdclemp1  12421  ndxid  12456  2strstr1g  12546  srgfcl  12969  toponrestid  13152  istpsi  13170  distopon  13220  distps  13224  discld  13269  txbas  13391  txdis  13410  txdis1cn  13411  txhmeo  13452  txswaphmeolem  13453  dvexp  13808  sinq34lt0t  13885  loge  13921  2logb9irr  14022  2logb9irrALT  14025  sqrt2cxp2logb9e3  14026  2logb9irrap  14028  lgsdir  14069  2sqlem9  14093  2sqlem10  14094  ex-ceil  14100  ex-gcd  14105  bj-charfundcALT  14183  bdceqir  14218  bj-ssom  14310  trilpolemgt1  14410  redcwlpolemeq1  14425