Theorem eqcomi 2197

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 2195	. 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 1458  ax-gen 1460  ax-ext 2175

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

This theorem is referenced by:  eqtr2i  2215  eqtr3i  2216  eqtr4i  2217  eqtr3id  2240  eqtr3di  2241  eqtr4di  2244  eqtr4id  2245  eqeltrri  2267  eleqtrri  2269  eqeltrrid  2281  eleqtrrdi  2287  abid2  2314  abid2f  2362  eqnetrri  2389  neeqtrri  2393  eqsstrri  3213  sseqtrri  3215  eqsstrrid  3227  sseqtrrdi  3229  difdif2ss  3417  inrab2  3433  dfopg  3803  opid  3823  eqbrtrri  4053  breqtrri  4057  breqtrrdi  4072  pwin  4314  limon  4546  tfis  4616  dfdm2  5201  cnvresid  5329  fores  5487  funcoeqres  5532  f1oprg  5545  fnmptfvd  5663  fmptpr  5751  fsnunres  5761  idref  5800  riotaprop  5898  fo1st  6212  fo2nd  6213  fnmpoovd  6270  ixpsnf1o  6792  phplem4  6913  snnen2og  6917  phplem4on  6925  pw1dc0el  6969  ss1o0el1o  6971  sbthlemi5  7022  eldju  7129  casefun  7146  omp1eomlem  7155  exmidfodomrlemim  7263  caucvgsrlembound  7856  ax0id  7940  1p1e2  9101  1e2m1  9103  2p1e3  9118  3p1e4  9120  4p1e5  9121  5p1e6  9122  6p1e7  9123  7p1e8  9124  8p1e9  9125  div4p1lem1div2  9239  0mnnnnn0  9275  zeo  9425  num0u  9461  numsucc  9490  decsucc  9491  1e0p1  9492  nummac  9495  decsubi  9513  decmul1  9514  decmul10add  9519  6p5lem  9520  10m1e9  9546  5t5e25  9553  6t6e36  9558  8t6e48  9569  decbin3  9592  infrenegsupex  9662  ige3m2fz  10118  fseq1p1m1  10163  fz0tp  10191  fz0to4untppr  10193  1fv  10208  fzo0to42pr  10290  fzosplitprm1  10304  fldiv4lem1div2uz2  10378  xnn0nnen  10511  expnegap0  10621  sq4e2t8  10711  3dec  10788  fihashen1  10873  pr0hash2ex  10889  imi  11047  infxrnegsupex  11409  zsumdc  11530  fsumadd  11552  hashrabrex  11627  ntrivcvgap  11694  fprodmul  11737  fproddivapf  11777  fprodmodd  11787  efsep  11837  3dvdsdec  12009  3dvds2dec  12010  flodddiv4  12078  lcmneg  12215  ennnfonelem1  12567  nninfdclemp1  12610  ndxid  12645  2strstr1g  12742  srgfcl  13472  isrhm  13657  issubrng  13698  rmodislmod  13850  cnfld0  14070  cnfld1  14071  cnfldplusf  14073  cnfldui  14088  toponrestid  14200  istpsi  14218  distopon  14266  distps  14270  discld  14315  txbas  14437  txdis  14456  txdis1cn  14457  txhmeo  14498  txswaphmeolem  14499  dvmptidcn  14893  dvmptid  14895  sinq34lt0t  15007  loge  15043  2logb9irr  15144  2logb9irrALT  15147  sqrt2cxp2logb9e3  15148  2logb9irrap  15150  lgsdir  15192  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3d1  15257  2lgsoddprmlem3d  15267  2sqlem9  15281  2sqlem10  15282  ex-ceil  15288  ex-gcd  15293  bj-charfundcALT  15371  bdceqir  15406  bj-ssom  15498  trilpolemgt1  15599  redcwlpolemeq1  15614