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  3776  opid  3796  eqbrtrri  4026  breqtrri  4030  breqtrrdi  4045  pwin  4282  limon  4512  tfis  4582  dfdm2  5163  cnvresid  5290  fores  5447  funcoeqres  5492  f1oprg  5505  fnmptfvd  5620  fmptpr  5708  fsnunres  5718  riotaprop  5853  fo1st  6157  fo2nd  6158  fnmpoovd  6215  ixpsnf1o  6735  phplem4  6854  snnen2og  6858  phplem4on  6866  pw1dc0el  6910  ss1o0el1o  6911  sbthlemi5  6959  eldju  7066  casefun  7083  omp1eomlem  7092  exmidfodomrlemim  7199  caucvgsrlembound  7792  ax0id  7876  1p1e2  9035  1e2m1  9037  2p1e3  9051  3p1e4  9053  4p1e5  9054  5p1e6  9055  6p1e7  9056  7p1e8  9057  8p1e9  9058  div4p1lem1div2  9171  0mnnnnn0  9207  zeo  9357  num0u  9393  numsucc  9422  decsucc  9423  1e0p1  9424  nummac  9427  decsubi  9445  decmul1  9446  decmul10add  9451  6p5lem  9452  10m1e9  9478  5t5e25  9485  6t6e36  9490  8t6e48  9501  decbin3  9524  infrenegsupex  9593  ige3m2fz  10048  fseq1p1m1  10093  fz0tp  10121  fz0to4untppr  10123  1fv  10138  fzo0to42pr  10219  fzosplitprm1  10233  expnegap0  10527  sq4e2t8  10617  3dec  10693  fihashen1  10778  pr0hash2ex  10794  imi  10908  infxrnegsupex  11270  zsumdc  11391  fsumadd  11413  hashrabrex  11488  ntrivcvgap  11555  fprodmul  11598  fproddivapf  11638  fprodmodd  11648  efsep  11698  3dvdsdec  11869  3dvds2dec  11870  flodddiv4  11938  lcmneg  12073  ennnfonelem1  12407  nninfdclemp1  12450  ndxid  12485  2strstr1g  12579  srgfcl  13154  cnfld0  13435  cnfld1  13436  cnfldplusf  13438  toponrestid  13491  istpsi  13509  distopon  13557  distps  13561  discld  13606  txbas  13728  txdis  13747  txdis1cn  13748  txhmeo  13789  txswaphmeolem  13790  dvexp  14145  sinq34lt0t  14222  loge  14258  2logb9irr  14359  2logb9irrALT  14362  sqrt2cxp2logb9e3  14363  2logb9irrap  14365  lgsdir  14406  2lgsoddprmlem3d  14428  2sqlem9  14441  2sqlem10  14442  ex-ceil  14448  ex-gcd  14453  bj-charfundcALT  14531  bdceqir  14566  bj-ssom  14658  trilpolemgt1  14757  redcwlpolemeq1  14772