Theorem eqcomi 2174

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

Syntax hints:   = wceq 1348

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 1440  ax-gen 1442  ax-ext 2152

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

This theorem is referenced by:  eqtr2i  2192  eqtr3i  2193  eqtr4i  2194  eqtr3id  2217  eqtr3di  2218  eqtr4di  2221  eqtr4id  2222  eqeltrri  2244  eleqtrri  2246  eqeltrrid  2258  eleqtrrdi  2264  abid2  2291  abid2f  2338  eqnetrri  2365  neeqtrri  2369  eqsstrri  3180  sseqtrri  3182  eqsstrrid  3194  sseqtrrdi  3196  difdif2ss  3384  inrab2  3400  dfopg  3763  opid  3783  eqbrtrri  4012  breqtrri  4016  breqtrrdi  4031  pwin  4267  limon  4497  tfis  4567  dfdm2  5145  cnvresid  5272  fores  5429  funcoeqres  5473  f1oprg  5486  fnmptfvd  5600  fmptpr  5688  fsnunres  5698  riotaprop  5832  fo1st  6136  fo2nd  6137  fnmpoovd  6194  ixpsnf1o  6714  phplem4  6833  snnen2og  6837  phplem4on  6845  pw1dc0el  6889  ss1o0el1o  6890  sbthlemi5  6938  eldju  7045  casefun  7062  omp1eomlem  7071  exmidfodomrlemim  7178  caucvgsrlembound  7756  ax0id  7840  1p1e2  8995  1e2m1  8997  2p1e3  9011  3p1e4  9013  4p1e5  9014  5p1e6  9015  6p1e7  9016  7p1e8  9017  8p1e9  9018  div4p1lem1div2  9131  0mnnnnn0  9167  zeo  9317  num0u  9353  numsucc  9382  decsucc  9383  1e0p1  9384  nummac  9387  decsubi  9405  decmul1  9406  decmul10add  9411  6p5lem  9412  10m1e9  9438  5t5e25  9445  6t6e36  9450  8t6e48  9461  decbin3  9484  infrenegsupex  9553  ige3m2fz  10005  fseq1p1m1  10050  fz0tp  10078  fz0to4untppr  10080  1fv  10095  fzo0to42pr  10176  fzosplitprm1  10190  expnegap0  10484  sq4e2t8  10573  3dec  10648  fihashen1  10734  pr0hash2ex  10750  imi  10864  infxrnegsupex  11226  zsumdc  11347  fsumadd  11369  hashrabrex  11444  ntrivcvgap  11511  fprodmul  11554  fproddivapf  11594  fprodmodd  11604  efsep  11654  3dvdsdec  11824  3dvds2dec  11825  flodddiv4  11893  lcmneg  12028  ennnfonelem1  12362  nninfdclemp1  12405  ndxid  12440  2strstr1g  12521  toponrestid  12813  istpsi  12831  distopon  12881  distps  12885  discld  12930  txbas  13052  txdis  13071  txdis1cn  13072  txhmeo  13113  txswaphmeolem  13114  dvexp  13469  sinq34lt0t  13546  loge  13582  2logb9irr  13683  2logb9irrALT  13686  sqrt2cxp2logb9e3  13687  2logb9irrap  13689  lgsdir  13730  2sqlem9  13754  2sqlem10  13755  ex-ceil  13761  ex-gcd  13766  bj-charfundcALT  13844  bdceqir  13879  bj-ssom  13971  trilpolemgt1  14071  redcwlpolemeq1  14086