Theorem eqcomi 2210

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

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-ext 2188

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

This theorem is referenced by:  eqtr2i  2228  eqtr3i  2229  eqtr4i  2230  eqtr3id  2253  eqtr3di  2254  eqtr4di  2257  eqtr4id  2258  eqeltrri  2280  eleqtrri  2282  eqeltrrid  2294  eleqtrrdi  2300  abid2  2327  abid2f  2375  eqnetrri  2402  neeqtrri  2406  eqsstrri  3230  sseqtrri  3232  eqsstrrid  3244  sseqtrrdi  3246  difdif2ss  3434  inrab2  3450  dfopg  3823  opid  3843  eqbrtrri  4074  breqtrri  4078  breqtrrdi  4093  opwo0id  4301  pwin  4337  limon  4569  tfis  4639  dfdm2  5226  cnvresid  5357  fores  5520  funcoeqres  5565  f1oprg  5579  fnmptfvd  5697  funopdmsn  5777  fmptpr  5789  fsnunres  5799  idref  5838  riotaprop  5936  fo1st  6256  fo2nd  6257  fnmpoovd  6314  ixpsnf1o  6836  phplem4  6967  snnen2og  6971  phplem4on  6979  pw1dc0el  7023  ss1o0el1o  7025  sbthlemi5  7078  eldju  7185  casefun  7202  omp1eomlem  7211  exmidfodomrlemim  7325  caucvgsrlembound  7927  ax0id  8011  1p1e2  9173  1e2m1  9175  2p1e3  9190  3p1e4  9192  4p1e5  9193  5p1e6  9194  6p1e7  9195  7p1e8  9196  8p1e9  9197  div4p1lem1div2  9311  0mnnnnn0  9347  zeo  9498  num0u  9534  numsucc  9563  decsucc  9564  1e0p1  9565  nummac  9568  decsubi  9586  decmul1  9587  decmul10add  9592  6p5lem  9593  10m1e9  9619  5t5e25  9626  6t6e36  9631  8t6e48  9642  decbin3  9665  infrenegsupex  9735  ige3m2fz  10191  fseq1p1m1  10236  fz0tp  10264  fz0to4untppr  10266  1fv  10281  fzo0to42pr  10371  fzosplitprm1  10385  fldiv4lem1div2uz2  10471  xnn0nnen  10604  expnegap0  10714  sq4e2t8  10804  3dec  10881  fihashen1  10966  pr0hash2ex  10982  fundm2domnop0  11012  imi  11286  infxrnegsupex  11649  zsumdc  11770  fsumadd  11792  hashrabrex  11867  ntrivcvgap  11934  fprodmul  11977  fproddivapf  12017  fprodmodd  12027  efsep  12077  3dvds  12250  3dvdsdec  12251  3dvds2dec  12252  flodddiv4  12322  lcmneg  12471  dec2dvds  12809  2exp5  12830  2exp11  12834  ennnfonelem1  12853  nninfdclemp1  12896  ndxid  12931  2strstr1g  13029  srgfcl  13810  isrhm  13995  issubrng  14036  rmodislmod  14188  cnfld0  14408  cnfld1  14409  cnfldplusf  14411  cnfldui  14426  toponrestid  14568  istpsi  14586  distopon  14634  distps  14638  discld  14683  txbas  14805  txdis  14824  txdis1cn  14825  txhmeo  14866  txswaphmeolem  14867  dvmptidcn  15261  dvmptid  15263  sinq34lt0t  15378  loge  15414  2logb9irr  15518  2logb9irrALT  15521  sqrt2cxp2logb9e3  15522  2logb9irrap  15524  lgsdir  15587  2lgslem3a  15645  2lgslem3b  15646  2lgslem3c  15647  2lgslem3d  15648  2lgslem3d1  15652  2lgsoddprmlem3d  15662  2sqlem9  15676  2sqlem10  15677  edgiedgbg  15736  edg0iedg0g  15737  isuhgrm  15742  isushgrm  15743  uhgr0  15756  isupgren  15766  isumgren  15776  ex-ceil  15801  ex-gcd  15806  bj-charfundcALT  15883  bdceqir  15918  bj-ssom  16010  trilpolemgt1  16119  redcwlpolemeq1  16134