Theorem eqcomi 2181

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

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  3189  sseqtrri  3191  eqsstrrid  3203  sseqtrrdi  3205  difdif2ss  3393  inrab2  3409  dfopg  3777  opid  3797  eqbrtrri  4027  breqtrri  4031  breqtrrdi  4046  pwin  4283  limon  4513  tfis  4583  dfdm2  5164  cnvresid  5291  fores  5448  funcoeqres  5493  f1oprg  5506  fnmptfvd  5621  fmptpr  5709  fsnunres  5719  riotaprop  5854  fo1st  6158  fo2nd  6159  fnmpoovd  6216  ixpsnf1o  6736  phplem4  6855  snnen2og  6859  phplem4on  6867  pw1dc0el  6911  ss1o0el1o  6912  sbthlemi5  6960  eldju  7067  casefun  7084  omp1eomlem  7093  exmidfodomrlemim  7200  caucvgsrlembound  7793  ax0id  7877  1p1e2  9036  1e2m1  9038  2p1e3  9052  3p1e4  9054  4p1e5  9055  5p1e6  9056  6p1e7  9057  7p1e8  9058  8p1e9  9059  div4p1lem1div2  9172  0mnnnnn0  9208  zeo  9358  num0u  9394  numsucc  9423  decsucc  9424  1e0p1  9425  nummac  9428  decsubi  9446  decmul1  9447  decmul10add  9452  6p5lem  9453  10m1e9  9479  5t5e25  9486  6t6e36  9491  8t6e48  9502  decbin3  9525  infrenegsupex  9594  ige3m2fz  10049  fseq1p1m1  10094  fz0tp  10122  fz0to4untppr  10124  1fv  10139  fzo0to42pr  10220  fzosplitprm1  10234  expnegap0  10528  sq4e2t8  10618  3dec  10694  fihashen1  10779  pr0hash2ex  10795  imi  10909  infxrnegsupex  11271  zsumdc  11392  fsumadd  11414  hashrabrex  11489  ntrivcvgap  11556  fprodmul  11599  fproddivapf  11639  fprodmodd  11649  efsep  11699  3dvdsdec  11870  3dvds2dec  11871  flodddiv4  11939  lcmneg  12074  ennnfonelem1  12408  nninfdclemp1  12451  ndxid  12486  2strstr1g  12580  srgfcl  13156  rmodislmod  13441  cnfld0  13468  cnfld1  13469  cnfldplusf  13471  toponrestid  13524  istpsi  13542  distopon  13590  distps  13594  discld  13639  txbas  13761  txdis  13780  txdis1cn  13781  txhmeo  13822  txswaphmeolem  13823  dvexp  14178  sinq34lt0t  14255  loge  14291  2logb9irr  14392  2logb9irrALT  14395  sqrt2cxp2logb9e3  14396  2logb9irrap  14398  lgsdir  14439  2lgsoddprmlem3d  14461  2sqlem9  14474  2sqlem10  14475  ex-ceil  14481  ex-gcd  14486  bj-charfundcALT  14564  bdceqir  14599  bj-ssom  14691  trilpolemgt1  14790  redcwlpolemeq1  14805