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  4154  breqtrri  4158  breqtrrdi  4173  opwo0id  4391  pwin  4429  limon  4662  tfis  4732  dfdm2  5325  cnvresid  5458  fores  5628  funcoeqres  5673  f1oprg  5688  fvmbr  5734  fnmptfvd  5816  funopdmsn  5898  fmptpr  5910  fsnunres  5920  idref  5965  riotaeqimp  6066  riotaprop  6067  fo1st  6395  fo2nd  6396  fnmpoovd  6455  ixpsnf1o  7024  phplem4  7162  snnen2og  7166  phplem4on  7175  pw1dc0el  7224  ss1o0el1o  7226  sbthlemi5  7285  eldju  7415  casefun  7432  omp1eomlem  7441  exmidfodomrlemim  7560  caucvgsrlembound  8168  ax0id  8252  1p1e2  9431  1e2m1  9433  2p1e3  9448  3p1e4  9450  4p1e5  9451  5p1e6  9452  6p1e7  9453  7p1e8  9454  8p1e9  9455  div4p1lem1div2  9571  0mnnnnn0  9607  zeo  9762  num0u  9798  numsucc  9832  decsucc  9833  1e0p1  9834  nummac  9837  decsubi  9855  decmul1  9856  decmul10add  9861  6p5lem  9862  10m1e9  9888  5t5e25  9895  6t6e36  9900  8t6e48  9911  decbin3  9934  infrenegsupex  10010  ige3m2fz  10471  fseq1p1m1  10518  fz0tp  10546  fz0to4untppr  10548  1fv  10563  fzo0to42pr  10655  fzosplitpr  10669  fzosplitprm1  10670  fldiv4lem1div2uz2  10762  xnn0nnen  10895  expnegap0  11005  sq4e2t8  11095  3dec  11174  fihashen1  11260  pr0hash2ex  11278  fundm2domnop0  11322  pfxccat3  11528  swrdccat  11529  pfxccatpfx2  11531  swrdccat3blem  11533  swrdccat3b  11534  cats2catd  11563  imi  11688  infxrnegsupex  12054  zsumdc  12176  fsumadd  12198  hashrabrex  12273  ntrivcvgap  12340  fprodmul  12383  fproddivapf  12423  fprodmodd  12433  efsep  12483  3dvds  12656  3dvdsdec  12657  3dvds2dec  12658  flodddiv4  12728  lcmneg  12877  dec2dvds  13219  2exp5  13241  2exp11  13245  1259prm  13276  ballotfilemth  13339  ennnfonelem1  13356  nninfdclemp1  13399  ndxid  13434  2strstr1g  13535  srgfcl  14384  isrhm  14574  issubrng  14616  rmodislmod  14797  cnfld0  15017  cnfld1  15018  cnfldplusf  15020  cnfldui  15033  isassa  15111  assamulgscmlem2  15151  toponrestid  15280  istpsi  15298  distopon  15346  distps  15350  discld  15395  txbas  15517  txdis  15536  txdis1cn  15537  txhmeo  15578  txswaphmeolem  15579  dvmptidcn  15973  dvmptid  15975  sinq34lt0t  16091  loge  16129  2logb9irr  16240  2logb9irrALT  16243  sqrt2cxp2logb9e3  16244  2logb9irrap  16246  birthdaylog2  16261  cht2  16309  cht3  16310  chtublem  16328  bclbnd  16340  bposlem6  16349  bposlem8  16351  lgsdir  16392  2lgslem3a  16450  2lgslem3b  16451  2lgslem3c  16452  2lgslem3d  16453  2lgslem3d1  16457  2lgsoddprmlem3d  16467  2sqlem9  16481  2sqlem10  16482  setsvtx  16530  edgiedgbg  16544  edg0iedg0g  16545  isuhgrm  16550  isushgrm  16551  uhgr0  16564  isupgren  16574  isumgren  16584  umgrpredgv  16626  isuspgren  16636  isusgren  16637  ausgrusgrben  16647  usgrf1oedg  16684  uhgr2edg  16685  usgredg3  16693  ushgredgedg  16705  ushgredgedgloop  16707  usgr0  16718  egrsubgr  16742  0grsubgr  16743  vtxdfifiun  16776  edginwlkd  16834  wlk1walkdom  16838  clwwlknon2x  16914  clwwlknonex2lem1  16916  konigsberglem1  16967  konigsberglem2  16968  konigsberglem3  16969  konigsberglem5  16971  ex-ceil  16978  ex-gcd  16983  bj-charfundcALT  17073  bdceqir  17108  bj-ssom  17200  trilpolemgt1  17328  redcwlpolemeq1  17344