Theorem eqcomi 2233

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-ext 2211

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

This theorem is referenced by:  eqtr2i  2251  eqtr3i  2252  eqtr4i  2253  eqtr3id  2276  eqtr3di  2277  eqtr4di  2280  eqtr4id  2281  eqeltrri  2303  eleqtrri  2305  eqeltrrid  2317  eleqtrrdi  2323  abid2  2350  abid2f  2398  eqnetrri  2425  neeqtrri  2429  eqsstrri  3257  sseqtrri  3259  eqsstrrid  3271  sseqtrrdi  3273  difdif2ss  3461  inrab2  3477  dfopg  3854  opid  3874  eqbrtrri  4105  breqtrri  4109  breqtrrdi  4124  opwo0id  4334  pwin  4370  limon  4602  tfis  4672  dfdm2  5259  cnvresid  5391  fores  5554  funcoeqres  5599  f1oprg  5613  fnmptfvd  5732  funopdmsn  5812  fmptpr  5824  fsnunres  5834  idref  5873  riotaeqimp  5972  riotaprop  5973  fo1st  6293  fo2nd  6294  fnmpoovd  6351  ixpsnf1o  6873  phplem4  7004  snnen2og  7008  phplem4on  7017  pw1dc0el  7061  ss1o0el1o  7063  sbthlemi5  7116  eldju  7223  casefun  7240  omp1eomlem  7249  exmidfodomrlemim  7367  caucvgsrlembound  7969  ax0id  8053  1p1e2  9215  1e2m1  9217  2p1e3  9232  3p1e4  9234  4p1e5  9235  5p1e6  9236  6p1e7  9237  7p1e8  9238  8p1e9  9239  div4p1lem1div2  9353  0mnnnnn0  9389  zeo  9540  num0u  9576  numsucc  9605  decsucc  9606  1e0p1  9607  nummac  9610  decsubi  9628  decmul1  9629  decmul10add  9634  6p5lem  9635  10m1e9  9661  5t5e25  9668  6t6e36  9673  8t6e48  9684  decbin3  9707  infrenegsupex  9777  ige3m2fz  10233  fseq1p1m1  10278  fz0tp  10306  fz0to4untppr  10308  1fv  10323  fzo0to42pr  10413  fzosplitprm1  10427  fldiv4lem1div2uz2  10513  xnn0nnen  10646  expnegap0  10756  sq4e2t8  10846  3dec  10923  fihashen1  11008  pr0hash2ex  11024  fundm2domnop0  11054  pfxccat3  11252  swrdccat  11253  pfxccatpfx2  11255  swrdccat3blem  11257  swrdccat3b  11258  cats2catd  11287  imi  11397  infxrnegsupex  11760  zsumdc  11881  fsumadd  11903  hashrabrex  11978  ntrivcvgap  12045  fprodmul  12088  fproddivapf  12128  fprodmodd  12138  efsep  12188  3dvds  12361  3dvdsdec  12362  3dvds2dec  12363  flodddiv4  12433  lcmneg  12582  dec2dvds  12920  2exp5  12941  2exp11  12945  ennnfonelem1  12964  nninfdclemp1  13007  ndxid  13042  2strstr1g  13141  srgfcl  13922  isrhm  14107  issubrng  14148  rmodislmod  14300  cnfld0  14520  cnfld1  14521  cnfldplusf  14523  cnfldui  14538  toponrestid  14680  istpsi  14698  distopon  14746  distps  14750  discld  14795  txbas  14917  txdis  14936  txdis1cn  14937  txhmeo  14978  txswaphmeolem  14979  dvmptidcn  15373  dvmptid  15375  sinq34lt0t  15490  loge  15526  2logb9irr  15630  2logb9irrALT  15633  sqrt2cxp2logb9e3  15634  2logb9irrap  15636  lgsdir  15699  2lgslem3a  15757  2lgslem3b  15758  2lgslem3c  15759  2lgslem3d  15760  2lgslem3d1  15764  2lgsoddprmlem3d  15774  2sqlem9  15788  2sqlem10  15789  setsvtx  15837  edgiedgbg  15850  edg0iedg0g  15851  isuhgrm  15856  isushgrm  15857  uhgr0  15870  isupgren  15880  isumgren  15890  umgrpredgv  15930  isuspgren  15940  isusgren  15941  ausgrusgrben  15951  usgrf1oedg  15988  uhgr2edg  15989  usgredg3  15997  ushgredgedg  16009  ushgredgedgloop  16011  ex-ceil  16020  ex-gcd  16025  bj-charfundcALT  16102  bdceqir  16137  bj-ssom  16229  trilpolemgt1  16338  redcwlpolemeq1  16353