Theorem eqcomi 2242

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2i  2260  eqtr3i  2261  eqtr4i  2262  eqtr3id  2285  eqtr3di  2286  eqtr4di  2289  eqtr4id  2290  eqeltrri  2312  eleqtrri  2314  eqeltrrid  2326  eleqtrrdi  2332  abid2  2361  abid2f  2418  eqnetrri  2445  neeqtrri  2449  eqsstrri  3281  sseqtrri  3283  eqsstrrid  3295  sseqtrrdi  3297  difdif2ss  3488  inrab2  3506  dfopg  3902  opid  3922  eqbrtrri  4153  breqtrri  4157  breqtrrdi  4172  opwo0id  4389  pwin  4427  limon  4660  tfis  4730  dfdm2  5322  cnvresid  5455  fores  5625  funcoeqres  5670  f1oprg  5685  fvmbr  5731  fnmptfvd  5813  funopdmsn  5895  fmptpr  5907  fsnunres  5917  idref  5962  riotaeqimp  6063  riotaprop  6064  fo1st  6391  fo2nd  6392  fnmpoovd  6451  ixpsnf1o  7018  phplem4  7156  snnen2og  7160  phplem4on  7169  pw1dc0el  7218  ss1o0el1o  7220  sbthlemi5  7278  eldju  7408  casefun  7425  omp1eomlem  7434  exmidfodomrlemim  7553  caucvgsrlembound  8161  ax0id  8245  1p1e2  9422  1e2m1  9424  2p1e3  9439  3p1e4  9441  4p1e5  9442  5p1e6  9443  6p1e7  9444  7p1e8  9445  8p1e9  9446  div4p1lem1div2  9561  0mnnnnn0  9597  zeo  9753  num0u  9789  numsucc  9818  decsucc  9819  1e0p1  9820  nummac  9823  decsubi  9841  decmul1  9842  decmul10add  9847  6p5lem  9848  10m1e9  9874  5t5e25  9881  6t6e36  9886  8t6e48  9897  decbin3  9920  infrenegsupex  9996  ige3m2fz  10456  fseq1p1m1  10503  fz0tp  10531  fz0to4untppr  10533  1fv  10548  fzo0to42pr  10640  fzosplitpr  10654  fzosplitprm1  10655  fldiv4lem1div2uz2  10743  xnn0nnen  10876  expnegap0  10986  sq4e2t8  11076  3dec  11154  fihashen1  11240  pr0hash2ex  11258  fundm2domnop0  11302  pfxccat3  11508  swrdccat  11509  pfxccatpfx2  11511  swrdccat3blem  11513  swrdccat3b  11514  cats2catd  11543  imi  11668  infxrnegsupex  12031  zsumdc  12153  fsumadd  12175  hashrabrex  12250  ntrivcvgap  12317  fprodmul  12360  fproddivapf  12400  fprodmodd  12410  efsep  12460  3dvds  12633  3dvdsdec  12634  3dvds2dec  12635  flodddiv4  12705  lcmneg  12854  dec2dvds  13192  2exp5  13213  2exp11  13217  ballotfilemth  13283  ennnfonelem1  13300  nninfdclemp1  13343  ndxid  13378  2strstr1g  13478  srgfcl  14279  isrhm  14467  issubrng  14509  rmodislmod  14690  cnfld0  14910  cnfld1  14911  cnfldplusf  14913  cnfldui  14926  isassa  15004  assamulgscmlem2  15044  toponrestid  15124  istpsi  15142  distopon  15190  distps  15194  discld  15239  txbas  15361  txdis  15380  txdis1cn  15381  txhmeo  15422  txswaphmeolem  15423  dvmptidcn  15817  dvmptid  15819  sinq34lt0t  15935  loge  15971  2logb9irr  16079  2logb9irrALT  16082  sqrt2cxp2logb9e3  16083  2logb9irrap  16085  birthdaylog2  16096  bclbnd  16127  lgsdir  16166  2lgslem3a  16224  2lgslem3b  16225  2lgslem3c  16226  2lgslem3d  16227  2lgslem3d1  16231  2lgsoddprmlem3d  16241  2sqlem9  16255  2sqlem10  16256  setsvtx  16304  edgiedgbg  16318  edg0iedg0g  16319  isuhgrm  16324  isushgrm  16325  uhgr0  16338  isupgren  16348  isumgren  16358  umgrpredgv  16400  isuspgren  16410  isusgren  16411  ausgrusgrben  16421  usgrf1oedg  16458  uhgr2edg  16459  usgredg3  16467  ushgredgedg  16479  ushgredgedgloop  16481  usgr0  16492  egrsubgr  16516  0grsubgr  16517  vtxdfifiun  16550  edginwlkd  16608  wlk1walkdom  16612  clwwlknon2x  16688  clwwlknonex2lem1  16690  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  konigsberglem5  16745  ex-ceil  16752  ex-gcd  16757  bj-charfundcALT  16847  bdceqir  16882  bj-ssom  16974  trilpolemgt1  17100  redcwlpolemeq1  17116