Theorem eqcomi 2235

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-ext 2213

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

This theorem is referenced by:  eqtr2i  2253  eqtr3i  2254  eqtr4i  2255  eqtr3id  2278  eqtr3di  2279  eqtr4di  2282  eqtr4id  2283  eqeltrri  2305  eleqtrri  2307  eqeltrrid  2319  eleqtrrdi  2325  abid2  2353  abid2f  2401  eqnetrri  2428  neeqtrri  2432  eqsstrri  3261  sseqtrri  3263  eqsstrrid  3275  sseqtrrdi  3277  difdif2ss  3466  inrab2  3482  dfopg  3865  opid  3885  eqbrtrri  4116  breqtrri  4120  breqtrrdi  4135  opwo0id  4347  pwin  4385  limon  4617  tfis  4687  dfdm2  5278  cnvresid  5411  fores  5578  funcoeqres  5623  f1oprg  5638  fvmbr  5683  fnmptfvd  5760  funopdmsn  5842  fmptpr  5854  fsnunres  5864  idref  5907  riotaeqimp  6006  riotaprop  6007  fo1st  6329  fo2nd  6330  fnmpoovd  6389  ixpsnf1o  6948  phplem4  7084  snnen2og  7088  phplem4on  7097  pw1dc0el  7146  ss1o0el1o  7148  sbthlemi5  7203  eldju  7310  casefun  7327  omp1eomlem  7336  exmidfodomrlemim  7455  caucvgsrlembound  8057  ax0id  8141  1p1e2  9303  1e2m1  9305  2p1e3  9320  3p1e4  9322  4p1e5  9323  5p1e6  9324  6p1e7  9325  7p1e8  9326  8p1e9  9327  div4p1lem1div2  9441  0mnnnnn0  9477  zeo  9628  num0u  9664  numsucc  9693  decsucc  9694  1e0p1  9695  nummac  9698  decsubi  9716  decmul1  9717  decmul10add  9722  6p5lem  9723  10m1e9  9749  5t5e25  9756  6t6e36  9761  8t6e48  9772  decbin3  9795  infrenegsupex  9871  ige3m2fz  10327  fseq1p1m1  10372  fz0tp  10400  fz0to4untppr  10402  1fv  10417  fzo0to42pr  10509  fzosplitpr  10523  fzosplitprm1  10524  fldiv4lem1div2uz2  10610  xnn0nnen  10743  expnegap0  10853  sq4e2t8  10943  3dec  11020  fihashen1  11105  pr0hash2ex  11123  fundm2domnop0  11156  pfxccat3  11362  swrdccat  11363  pfxccatpfx2  11365  swrdccat3blem  11367  swrdccat3b  11368  cats2catd  11397  imi  11521  infxrnegsupex  11884  zsumdc  12006  fsumadd  12028  hashrabrex  12103  ntrivcvgap  12170  fprodmul  12213  fproddivapf  12253  fprodmodd  12263  efsep  12313  3dvds  12486  3dvdsdec  12487  3dvds2dec  12488  flodddiv4  12558  lcmneg  12707  dec2dvds  13045  2exp5  13066  2exp11  13070  ennnfonelem1  13089  nninfdclemp1  13132  ndxid  13167  2strstr1g  13266  srgfcl  14048  isrhm  14234  issubrng  14275  rmodislmod  14427  cnfld0  14647  cnfld1  14648  cnfldplusf  14650  cnfldui  14665  toponrestid  14812  istpsi  14830  distopon  14878  distps  14882  discld  14927  txbas  15049  txdis  15068  txdis1cn  15069  txhmeo  15110  txswaphmeolem  15111  dvmptidcn  15505  dvmptid  15507  sinq34lt0t  15622  loge  15658  2logb9irr  15762  2logb9irrALT  15765  sqrt2cxp2logb9e3  15766  2logb9irrap  15768  lgsdir  15834  2lgslem3a  15892  2lgslem3b  15893  2lgslem3c  15894  2lgslem3d  15895  2lgslem3d1  15899  2lgsoddprmlem3d  15909  2sqlem9  15923  2sqlem10  15924  setsvtx  15972  edgiedgbg  15986  edg0iedg0g  15987  isuhgrm  15992  isushgrm  15993  uhgr0  16006  isupgren  16016  isumgren  16026  umgrpredgv  16068  isuspgren  16078  isusgren  16079  ausgrusgrben  16089  usgrf1oedg  16126  uhgr2edg  16127  usgredg3  16135  ushgredgedg  16147  ushgredgedgloop  16149  usgr0  16160  egrsubgr  16184  0grsubgr  16185  vtxdfifiun  16218  edginwlkd  16276  wlk1walkdom  16280  clwwlknon2x  16356  clwwlknonex2lem1  16358  konigsberglem1  16409  konigsberglem2  16410  konigsberglem3  16411  konigsberglem5  16413  ex-ceil  16420  ex-gcd  16425  bj-charfundcALT  16505  bdceqir  16540  bj-ssom  16632  trilpolemgt1  16751  redcwlpolemeq1  16767