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  3188  sseqtrri  3190  eqsstrrid  3202  sseqtrrdi  3204  difdif2ss  3392  inrab2  3408  dfopg  3775  opid  3795  eqbrtrri  4024  breqtrri  4028  breqtrrdi  4043  pwin  4280  limon  4510  tfis  4580  dfdm2  5160  cnvresid  5287  fores  5444  funcoeqres  5489  f1oprg  5502  fnmptfvd  5617  fmptpr  5705  fsnunres  5715  riotaprop  5849  fo1st  6153  fo2nd  6154  fnmpoovd  6211  ixpsnf1o  6731  phplem4  6850  snnen2og  6854  phplem4on  6862  pw1dc0el  6906  ss1o0el1o  6907  sbthlemi5  6955  eldju  7062  casefun  7079  omp1eomlem  7088  exmidfodomrlemim  7195  caucvgsrlembound  7788  ax0id  7872  1p1e2  9030  1e2m1  9032  2p1e3  9046  3p1e4  9048  4p1e5  9049  5p1e6  9050  6p1e7  9051  7p1e8  9052  8p1e9  9053  div4p1lem1div2  9166  0mnnnnn0  9202  zeo  9352  num0u  9388  numsucc  9417  decsucc  9418  1e0p1  9419  nummac  9422  decsubi  9440  decmul1  9441  decmul10add  9446  6p5lem  9447  10m1e9  9473  5t5e25  9480  6t6e36  9485  8t6e48  9496  decbin3  9519  infrenegsupex  9588  ige3m2fz  10042  fseq1p1m1  10087  fz0tp  10115  fz0to4untppr  10117  1fv  10132  fzo0to42pr  10213  fzosplitprm1  10227  expnegap0  10521  sq4e2t8  10610  3dec  10685  fihashen1  10770  pr0hash2ex  10786  imi  10900  infxrnegsupex  11262  zsumdc  11383  fsumadd  11405  hashrabrex  11480  ntrivcvgap  11547  fprodmul  11590  fproddivapf  11630  fprodmodd  11640  efsep  11690  3dvdsdec  11860  3dvds2dec  11861  flodddiv4  11929  lcmneg  12064  ennnfonelem1  12398  nninfdclemp1  12441  ndxid  12476  2strstr1g  12570  srgfcl  13056  cnfld0  13270  cnfld1  13271  cnfldplusf  13273  toponrestid  13301  istpsi  13319  distopon  13369  distps  13373  discld  13418  txbas  13540  txdis  13559  txdis1cn  13560  txhmeo  13601  txswaphmeolem  13602  dvexp  13957  sinq34lt0t  14034  loge  14070  2logb9irr  14171  2logb9irrALT  14174  sqrt2cxp2logb9e3  14175  2logb9irrap  14177  lgsdir  14218  2sqlem9  14242  2sqlem10  14243  ex-ceil  14249  ex-gcd  14254  bj-charfundcALT  14332  bdceqir  14367  bj-ssom  14459  trilpolemgt1  14558  redcwlpolemeq1  14573