Theorem eqcomi 2169

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-ext 2147

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

This theorem is referenced by:  eqtr2i  2187  eqtr3i  2188  eqtr4i  2189  eqtr3id  2212  eqtr3di  2213  eqtr4di  2216  eqtr4id  2217  eqeltrri  2239  eleqtrri  2241  eqeltrrid  2253  eleqtrrdi  2259  abid2  2286  abid2f  2333  eqnetrri  2360  neeqtrri  2364  eqsstrri  3174  sseqtrri  3176  eqsstrrid  3188  sseqtrrdi  3190  difdif2ss  3378  inrab2  3394  dfopg  3755  opid  3775  eqbrtrri  4004  breqtrri  4008  breqtrrdi  4023  pwin  4259  limon  4489  tfis  4559  dfdm2  5137  cnvresid  5261  fores  5418  funcoeqres  5462  f1oprg  5475  fmptpr  5676  fsnunres  5686  riotaprop  5820  fo1st  6122  fo2nd  6123  fnmpoovd  6179  ixpsnf1o  6698  phplem4  6817  snnen2og  6821  phplem4on  6829  pw1dc0el  6873  ss1o0el1o  6874  sbthlemi5  6922  eldju  7029  casefun  7046  omp1eomlem  7055  exmidfodomrlemim  7153  caucvgsrlembound  7731  ax0id  7815  1p1e2  8970  1e2m1  8972  2p1e3  8986  3p1e4  8988  4p1e5  8989  5p1e6  8990  6p1e7  8991  7p1e8  8992  8p1e9  8993  div4p1lem1div2  9106  0mnnnnn0  9142  zeo  9292  num0u  9328  numsucc  9357  decsucc  9358  1e0p1  9359  nummac  9362  decsubi  9380  decmul1  9381  decmul10add  9386  6p5lem  9387  10m1e9  9413  5t5e25  9420  6t6e36  9425  8t6e48  9436  decbin3  9459  infrenegsupex  9528  ige3m2fz  9980  fseq1p1m1  10025  fz0tp  10053  fz0to4untppr  10055  1fv  10070  fzo0to42pr  10151  fzosplitprm1  10165  expnegap0  10459  sq4e2t8  10548  3dec  10623  fihashen1  10708  pr0hash2ex  10724  imi  10838  infxrnegsupex  11200  zsumdc  11321  fsumadd  11343  hashrabrex  11418  ntrivcvgap  11485  fprodmul  11528  fproddivapf  11568  fprodmodd  11578  efsep  11628  3dvdsdec  11798  3dvds2dec  11799  flodddiv4  11867  lcmneg  12002  ennnfonelem1  12336  nninfdclemp1  12379  ndxid  12414  2strstr1g  12493  toponrestid  12619  istpsi  12637  distopon  12687  distps  12691  discld  12736  txbas  12858  txdis  12877  txdis1cn  12878  txhmeo  12919  txswaphmeolem  12920  dvexp  13275  sinq34lt0t  13352  loge  13388  2logb9irr  13489  2logb9irrALT  13492  sqrt2cxp2logb9e3  13493  2logb9irrap  13495  lgsdir  13536  2sqlem9  13560  2sqlem10  13561  ex-ceil  13567  ex-gcd  13572  bj-charfundcALT  13651  bdceqir  13686  bj-ssom  13778  trilpolemgt1  13878  redcwlpolemeq1  13893