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 ⊢ 𝐵 = 𝐴

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-ext 2220

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

This theorem is referenced 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  3900  opid  3920  eqbrtrri  4151  breqtrri  4155  breqtrrdi  4170  opwo0id  4387  pwin  4425  limon  4658  tfis  4728  dfdm2  5320  cnvresid  5453  fores  5623  funcoeqres  5668  f1oprg  5683  fvmbr  5728  fnmptfvd  5807  funopdmsn  5889  fmptpr  5901  fsnunres  5911  idref  5956  riotaeqimp  6057  riotaprop  6058  fo1st  6385  fo2nd  6386  fnmpoovd  6445  ixpsnf1o  7012  phplem4  7150  snnen2og  7154  phplem4on  7163  pw1dc0el  7212  ss1o0el1o  7214  sbthlemi5  7272  eldju  7402  casefun  7419  omp1eomlem  7428  exmidfodomrlemim  7547  caucvgsrlembound  8155  ax0id  8239  1p1e2  9404  1e2m1  9406  2p1e3  9421  3p1e4  9423  4p1e5  9424  5p1e6  9425  6p1e7  9426  7p1e8  9427  8p1e9  9428  div4p1lem1div2  9542  0mnnnnn0  9578  zeo  9734  num0u  9770  numsucc  9799  decsucc  9800  1e0p1  9801  nummac  9804  decsubi  9822  decmul1  9823  decmul10add  9828  6p5lem  9829  10m1e9  9855  5t5e25  9862  6t6e36  9867  8t6e48  9878  decbin3  9901  infrenegsupex  9977  ige3m2fz  10437  fseq1p1m1  10484  fz0tp  10512  fz0to4untppr  10514  1fv  10529  fzo0to42pr  10621  fzosplitpr  10635  fzosplitprm1  10636  fldiv4lem1div2uz2  10724  xnn0nnen  10857  expnegap0  10967  sq4e2t8  11057  3dec  11135  fihashen1  11221  pr0hash2ex  11239  fundm2domnop0  11283  pfxccat3  11489  swrdccat  11490  pfxccatpfx2  11492  swrdccat3blem  11494  swrdccat3b  11495  cats2catd  11524  imi  11649  infxrnegsupex  12012  zsumdc  12134  fsumadd  12156  hashrabrex  12231  ntrivcvgap  12298  fprodmul  12341  fproddivapf  12381  fprodmodd  12391  efsep  12441  3dvds  12614  3dvdsdec  12615  3dvds2dec  12616  flodddiv4  12686  lcmneg  12835  dec2dvds  13173  2exp5  13194  2exp11  13198  ballotfilemth  13264  ennnfonelem1  13281  nninfdclemp1  13324  ndxid  13359  2strstr1g  13459  srgfcl  14260  isrhm  14448  issubrng  14490  rmodislmod  14671  cnfld0  14891  cnfld1  14892  cnfldplusf  14894  cnfldui  14907  isassa  14985  assamulgscmlem2  15025  toponrestid  15105  istpsi  15123  distopon  15171  distps  15175  discld  15220  txbas  15342  txdis  15361  txdis1cn  15362  txhmeo  15403  txswaphmeolem  15404  dvmptidcn  15798  dvmptid  15800  sinq34lt0t  15915  loge  15951  2logb9irr  16056  2logb9irrALT  16059  sqrt2cxp2logb9e3  16060  2logb9irrap  16062  birthdaylog2  16073  lgsdir  16137  2lgslem3a  16195  2lgslem3b  16196  2lgslem3c  16197  2lgslem3d  16198  2lgslem3d1  16202  2lgsoddprmlem3d  16212  2sqlem9  16226  2sqlem10  16227  setsvtx  16275  edgiedgbg  16289  edg0iedg0g  16290  isuhgrm  16295  isushgrm  16296  uhgr0  16309  isupgren  16319  isumgren  16329  umgrpredgv  16371  isuspgren  16381  isusgren  16382  ausgrusgrben  16392  usgrf1oedg  16429  uhgr2edg  16430  usgredg3  16438  ushgredgedg  16450  ushgredgedgloop  16452  usgr0  16463  egrsubgr  16487  0grsubgr  16488  vtxdfifiun  16521  edginwlkd  16579  wlk1walkdom  16583  clwwlknon2x  16659  clwwlknonex2lem1  16661  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  konigsberglem5  16716  ex-ceil  16723  ex-gcd  16728  bj-charfundcALT  16818  bdceqir  16853  bj-ssom  16945  trilpolemgt1  17062  redcwlpolemeq1  17078