Theorem eqcomi 2200

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 2198	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	mpbi 145	1 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189

This theorem is referenced by:  eqtr2i  2218  eqtr3i  2219  eqtr4i  2220  eqtr3id  2243  eqtr3di  2244  eqtr4di  2247  eqtr4id  2248  eqeltrri  2270  eleqtrri  2272  eqeltrrid  2284  eleqtrrdi  2290  abid2  2317  abid2f  2365  eqnetrri  2392  neeqtrri  2396  eqsstrri  3216  sseqtrri  3218  eqsstrrid  3230  sseqtrrdi  3232  difdif2ss  3420  inrab2  3436  dfopg  3806  opid  3826  eqbrtrri  4056  breqtrri  4060  breqtrrdi  4075  pwin  4317  limon  4549  tfis  4619  dfdm2  5204  cnvresid  5332  fores  5490  funcoeqres  5535  f1oprg  5548  fnmptfvd  5666  fmptpr  5754  fsnunres  5764  idref  5803  riotaprop  5901  fo1st  6215  fo2nd  6216  fnmpoovd  6273  ixpsnf1o  6795  phplem4  6916  snnen2og  6920  phplem4on  6928  pw1dc0el  6972  ss1o0el1o  6974  sbthlemi5  7027  eldju  7134  casefun  7151  omp1eomlem  7160  exmidfodomrlemim  7268  caucvgsrlembound  7861  ax0id  7945  1p1e2  9107  1e2m1  9109  2p1e3  9124  3p1e4  9126  4p1e5  9127  5p1e6  9128  6p1e7  9129  7p1e8  9130  8p1e9  9131  div4p1lem1div2  9245  0mnnnnn0  9281  zeo  9431  num0u  9467  numsucc  9496  decsucc  9497  1e0p1  9498  nummac  9501  decsubi  9519  decmul1  9520  decmul10add  9525  6p5lem  9526  10m1e9  9552  5t5e25  9559  6t6e36  9564  8t6e48  9575  decbin3  9598  infrenegsupex  9668  ige3m2fz  10124  fseq1p1m1  10169  fz0tp  10197  fz0to4untppr  10199  1fv  10214  fzo0to42pr  10296  fzosplitprm1  10310  fldiv4lem1div2uz2  10396  xnn0nnen  10529  expnegap0  10639  sq4e2t8  10729  3dec  10806  fihashen1  10891  pr0hash2ex  10907  imi  11065  infxrnegsupex  11428  zsumdc  11549  fsumadd  11571  hashrabrex  11646  ntrivcvgap  11713  fprodmul  11756  fproddivapf  11796  fprodmodd  11806  efsep  11856  3dvds  12029  3dvdsdec  12030  3dvds2dec  12031  flodddiv4  12101  lcmneg  12242  dec2dvds  12580  2exp5  12601  2exp11  12605  ennnfonelem1  12624  nninfdclemp1  12667  ndxid  12702  2strstr1g  12799  srgfcl  13529  isrhm  13714  issubrng  13755  rmodislmod  13907  cnfld0  14127  cnfld1  14128  cnfldplusf  14130  cnfldui  14145  toponrestid  14257  istpsi  14275  distopon  14323  distps  14327  discld  14372  txbas  14494  txdis  14513  txdis1cn  14514  txhmeo  14555  txswaphmeolem  14556  dvmptidcn  14950  dvmptid  14952  sinq34lt0t  15067  loge  15103  2logb9irr  15207  2logb9irrALT  15210  sqrt2cxp2logb9e3  15211  2logb9irrap  15213  lgsdir  15276  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgslem3d1  15341  2lgsoddprmlem3d  15351  2sqlem9  15365  2sqlem10  15366  ex-ceil  15372  ex-gcd  15377  bj-charfundcALT  15455  bdceqir  15490  bj-ssom  15582  trilpolemgt1  15683  redcwlpolemeq1  15698