Theorem eqcomi 2143

Description: Inference from commutative law for class equality. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
eqcomi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqcomi	⊢ 𝐵 = 𝐴

Proof of Theorem eqcomi

Step	Hyp	Ref	Expression
1		eqcomi.1	. 2 ⊢ 𝐴 = 𝐵
2		eqcom 2141	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 144	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1331

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 1423  ax-gen 1425  ax-ext 2121

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

This theorem is referenced by:  eqtr2i  2161  eqtr3i  2162  eqtr4i  2163  syl5eqr  2186  syl5reqr  2187  syl6eqr  2190  syl6reqr  2191  eqeltrri  2213  eleqtrri  2215  eqeltrrid  2227  eleqtrrdi  2233  abid2  2260  abid2f  2306  eqnetrri  2333  neeqtrri  2337  eqsstrri  3130  sseqtrri  3132  eqsstrrid  3144  sseqtrrdi  3146  difdif2ss  3333  inrab2  3349  dfopg  3703  opid  3723  eqbrtrri  3951  breqtrri  3955  breqtrrdi  3970  pwin  4204  limon  4429  tfis  4497  dfdm2  5073  cnvresid  5197  fores  5354  funcoeqres  5398  f1oprg  5411  fmptpr  5612  fsnunres  5622  riotaprop  5753  fo1st  6055  fo2nd  6056  fnmpoovd  6112  ixpsnf1o  6630  phplem4  6749  snnen2og  6753  phplem4on  6761  sbthlemi5  6849  eldju  6953  casefun  6970  omp1eomlem  6979  exmidfodomrlemim  7057  caucvgsrlembound  7602  ax0id  7686  1p1e2  8837  1e2m1  8839  2p1e3  8853  3p1e4  8855  4p1e5  8856  5p1e6  8857  6p1e7  8858  7p1e8  8859  8p1e9  8860  div4p1lem1div2  8973  0mnnnnn0  9009  zeo  9156  num0u  9192  numsucc  9221  decsucc  9222  1e0p1  9223  nummac  9226  decsubi  9244  decmul1  9245  decmul10add  9250  6p5lem  9251  10m1e9  9277  5t5e25  9284  6t6e36  9289  8t6e48  9300  decbin3  9323  infrenegsupex  9389  ige3m2fz  9829  fseq1p1m1  9874  fz0tp  9901  1fv  9916  fzo0to42pr  9997  fzosplitprm1  10011  expnegap0  10301  sq4e2t8  10390  3dec  10461  fihashen1  10545  pr0hash2ex  10561  imi  10672  infxrnegsupex  11032  zsumdc  11153  fsumadd  11175  hashrabrex  11250  ntrivcvgap  11317  efsep  11397  3dvdsdec  11562  3dvds2dec  11563  flodddiv4  11631  lcmneg  11755  ennnfonelem1  11920  ndxid  11983  2strstr1g  12062  toponrestid  12188  istpsi  12206  distopon  12256  distps  12260  discld  12305  txbas  12427  txdis  12446  txdis1cn  12447  txhmeo  12488  txswaphmeolem  12489  dvexp  12844  sinq34lt0t  12912  ex-ceil  12938  ex-gcd  12943  bdceqir  13042  bj-ssom  13134  trilpolemgt1  13232