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  5623  fmptpr  5711  fsnunres  5721  riotaprop  5857  fo1st  6161  fo2nd  6162  fnmpoovd  6219  ixpsnf1o  6739  phplem4  6858  snnen2og  6862  phplem4on  6870  pw1dc0el  6914  ss1o0el1o  6915  sbthlemi5  6963  eldju  7070  casefun  7087  omp1eomlem  7096  exmidfodomrlemim  7203  caucvgsrlembound  7796  ax0id  7880  1p1e2  9039  1e2m1  9041  2p1e3  9055  3p1e4  9057  4p1e5  9058  5p1e6  9059  6p1e7  9060  7p1e8  9061  8p1e9  9062  div4p1lem1div2  9175  0mnnnnn0  9211  zeo  9361  num0u  9397  numsucc  9426  decsucc  9427  1e0p1  9428  nummac  9431  decsubi  9449  decmul1  9450  decmul10add  9455  6p5lem  9456  10m1e9  9482  5t5e25  9489  6t6e36  9494  8t6e48  9505  decbin3  9528  infrenegsupex  9597  ige3m2fz  10052  fseq1p1m1  10097  fz0tp  10125  fz0to4untppr  10127  1fv  10142  fzo0to42pr  10223  fzosplitprm1  10237  expnegap0  10531  sq4e2t8  10621  3dec  10697  fihashen1  10782  pr0hash2ex  10798  imi  10912  infxrnegsupex  11274  zsumdc  11395  fsumadd  11417  hashrabrex  11492  ntrivcvgap  11559  fprodmul  11602  fproddivapf  11642  fprodmodd  11652  efsep  11702  3dvdsdec  11873  3dvds2dec  11874  flodddiv4  11942  lcmneg  12077  ennnfonelem1  12411  nninfdclemp1  12454  ndxid  12489  2strstr1g  12583  srgfcl  13162  rmodislmod  13447  cnfld0  13605  cnfld1  13606  cnfldplusf  13608  toponrestid  13661  istpsi  13679  distopon  13727  distps  13731  discld  13776  txbas  13898  txdis  13917  txdis1cn  13918  txhmeo  13959  txswaphmeolem  13960  dvexp  14315  sinq34lt0t  14392  loge  14428  2logb9irr  14529  2logb9irrALT  14532  sqrt2cxp2logb9e3  14533  2logb9irrap  14535  lgsdir  14576  2lgsoddprmlem3d  14598  2sqlem9  14611  2sqlem10  14612  ex-ceil  14618  ex-gcd  14623  bj-charfundcALT  14701  bdceqir  14736  bj-ssom  14828  trilpolemgt1  14928  redcwlpolemeq1  14943