Theorem eqcomi 2104

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 2102	. 2 |- ( A = B <-> B = A )
3	1, 2	mpbi 144	1 |- B = A

Syntax hints:   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  eqtr2i  2121  eqtr3i  2122  eqtr4i  2123  syl5eqr  2146  syl5reqr  2147  syl6eqr  2150  syl6reqr  2151  eqeltrri  2173  eleqtrri  2175  syl5eqelr  2187  syl6eleqr  2193  abid2  2220  abid2f  2265  eqnetrri  2292  neeqtrri  2296  eqsstr3i  3080  sseqtr4i  3082  syl5eqssr  3094  syl6sseqr  3096  difdif2ss  3280  inrab2  3296  dfopg  3650  opid  3670  eqbrtrri  3896  breqtrri  3900  syl6breqr  3915  pwin  4142  limon  4367  tfis  4435  dfdm2  5009  cnvresid  5133  fores  5290  funcoeqres  5332  f1oprg  5343  fmptpr  5544  fsnunres  5554  riotaprop  5685  fo1st  5986  fo2nd  5987  fnmpoovd  6042  ixpsnf1o  6560  phplem4  6678  snnen2og  6682  phplem4on  6690  sbthlemi5  6777  eldju  6868  casefun  6885  omp1eomlem  6894  exmidfodomrlemim  6966  caucvgsrlembound  7489  ax0id  7563  1p1e2  8695  1e2m1  8697  2p1e3  8705  3p1e4  8707  4p1e5  8708  5p1e6  8709  6p1e7  8710  7p1e8  8711  8p1e9  8712  div4p1lem1div2  8825  0mnnnnn0  8861  zeo  9008  num0u  9044  numsucc  9073  decsucc  9074  1e0p1  9075  nummac  9078  decsubi  9096  decmul1  9097  decmul10add  9102  6p5lem  9103  10m1e9  9129  5t5e25  9136  6t6e36  9141  8t6e48  9152  decbin3  9175  infrenegsupex  9239  ige3m2fz  9670  fseq1p1m1  9715  fz0tp  9742  1fv  9757  fzo0to42pr  9838  fzosplitprm1  9852  expnegap0  10142  sq4e2t8  10231  3dec  10302  fihashen1  10386  pr0hash2ex  10402  imi  10513  infxrnegsupex  10871  zsumdc  10992  fsumadd  11014  hashrabrex  11089  efsep  11195  3dvdsdec  11357  3dvds2dec  11358  flodddiv4  11426  lcmneg  11548  ennnfonelem1  11712  ndxid  11765  2strstr1g  11844  toponrestid  11970  istpsi  11988  distopon  12038  distps  12042  discld  12087  txbas  12208  txdis  12227  txdis1cn  12228  ex-ceil  12541  ex-gcd  12546  bdceqir  12623  bj-ssom  12719  trilpolemgt1  12816