Theorem eqcomi 2141

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

Syntax hints:   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ext 2119

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

This theorem is referenced by:  eqtr2i  2159  eqtr3i  2160  eqtr4i  2161  syl5eqr  2184  syl5reqr  2185  syl6eqr  2188  syl6reqr  2189  eqeltrri  2211  eleqtrri  2213  eqeltrrid  2225  eleqtrrdi  2231  abid2  2258  abid2f  2304  eqnetrri  2331  neeqtrri  2335  eqsstrri  3125  sseqtrri  3127  eqsstrrid  3139  sseqtrrdi  3141  difdif2ss  3328  inrab2  3344  dfopg  3698  opid  3718  eqbrtrri  3946  breqtrri  3950  breqtrrdi  3965  pwin  4199  limon  4424  tfis  4492  dfdm2  5068  cnvresid  5192  fores  5349  funcoeqres  5391  f1oprg  5404  fmptpr  5605  fsnunres  5615  riotaprop  5746  fo1st  6048  fo2nd  6049  fnmpoovd  6105  ixpsnf1o  6623  phplem4  6742  snnen2og  6746  phplem4on  6754  sbthlemi5  6842  eldju  6946  casefun  6963  omp1eomlem  6972  exmidfodomrlemim  7050  caucvgsrlembound  7595  ax0id  7679  1p1e2  8830  1e2m1  8832  2p1e3  8846  3p1e4  8848  4p1e5  8849  5p1e6  8850  6p1e7  8851  7p1e8  8852  8p1e9  8853  div4p1lem1div2  8966  0mnnnnn0  9002  zeo  9149  num0u  9185  numsucc  9214  decsucc  9215  1e0p1  9216  nummac  9219  decsubi  9237  decmul1  9238  decmul10add  9243  6p5lem  9244  10m1e9  9270  5t5e25  9277  6t6e36  9282  8t6e48  9293  decbin3  9316  infrenegsupex  9382  ige3m2fz  9822  fseq1p1m1  9867  fz0tp  9894  1fv  9909  fzo0to42pr  9990  fzosplitprm1  10004  expnegap0  10294  sq4e2t8  10383  3dec  10454  fihashen1  10538  pr0hash2ex  10554  imi  10665  infxrnegsupex  11025  zsumdc  11146  fsumadd  11168  hashrabrex  11243  ntrivcvgap  11310  efsep  11386  3dvdsdec  11551  3dvds2dec  11552  flodddiv4  11620  lcmneg  11744  ennnfonelem1  11909  ndxid  11972  2strstr1g  12051  toponrestid  12177  istpsi  12195  distopon  12245  distps  12249  discld  12294  txbas  12416  txdis  12435  txdis1cn  12436  txhmeo  12477  txswaphmeolem  12478  dvexp  12833  sinq34lt0t  12901  ex-ceil  12927  ex-gcd  12932  bdceqir  13031  bj-ssom  13123  trilpolemgt1  13221