Theorem eqcomi 2181

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

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  3190  sseqtrri  3192  eqsstrrid  3204  sseqtrrdi  3206  difdif2ss  3394  inrab2  3410  dfopg  3778  opid  3798  eqbrtrri  4028  breqtrri  4032  breqtrrdi  4047  pwin  4284  limon  4514  tfis  4584  dfdm2  5165  cnvresid  5292  fores  5449  funcoeqres  5494  f1oprg  5507  fnmptfvd  5622  fmptpr  5710  fsnunres  5720  riotaprop  5856  fo1st  6160  fo2nd  6161  fnmpoovd  6218  ixpsnf1o  6738  phplem4  6857  snnen2og  6861  phplem4on  6869  pw1dc0el  6913  ss1o0el1o  6914  sbthlemi5  6962  eldju  7069  casefun  7086  omp1eomlem  7095  exmidfodomrlemim  7202  caucvgsrlembound  7795  ax0id  7879  1p1e2  9038  1e2m1  9040  2p1e3  9054  3p1e4  9056  4p1e5  9057  5p1e6  9058  6p1e7  9059  7p1e8  9060  8p1e9  9061  div4p1lem1div2  9174  0mnnnnn0  9210  zeo  9360  num0u  9396  numsucc  9425  decsucc  9426  1e0p1  9427  nummac  9430  decsubi  9448  decmul1  9449  decmul10add  9454  6p5lem  9455  10m1e9  9481  5t5e25  9488  6t6e36  9493  8t6e48  9504  decbin3  9527  infrenegsupex  9596  ige3m2fz  10051  fseq1p1m1  10096  fz0tp  10124  fz0to4untppr  10126  1fv  10141  fzo0to42pr  10222  fzosplitprm1  10236  expnegap0  10530  sq4e2t8  10620  3dec  10696  fihashen1  10781  pr0hash2ex  10797  imi  10911  infxrnegsupex  11273  zsumdc  11394  fsumadd  11416  hashrabrex  11491  ntrivcvgap  11558  fprodmul  11601  fproddivapf  11641  fprodmodd  11651  efsep  11701  3dvdsdec  11872  3dvds2dec  11873  flodddiv4  11941  lcmneg  12076  ennnfonelem1  12410  nninfdclemp1  12453  ndxid  12488  2strstr1g  12582  srgfcl  13161  rmodislmod  13446  cnfld0  13550  cnfld1  13551  cnfldplusf  13553  toponrestid  13606  istpsi  13624  distopon  13672  distps  13676  discld  13721  txbas  13843  txdis  13862  txdis1cn  13863  txhmeo  13904  txswaphmeolem  13905  dvexp  14260  sinq34lt0t  14337  loge  14373  2logb9irr  14474  2logb9irrALT  14477  sqrt2cxp2logb9e3  14478  2logb9irrap  14480  lgsdir  14521  2lgsoddprmlem3d  14543  2sqlem9  14556  2sqlem10  14557  ex-ceil  14563  ex-gcd  14568  bj-charfundcALT  14646  bdceqir  14681  bj-ssom  14773  trilpolemgt1  14872  redcwlpolemeq1  14887