Theorem eqcomi 2238

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 2236	. 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 2216

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

This theorem is referenced by:  eqtr2i  2256  eqtr3i  2257  eqtr4i  2258  eqtr3id  2281  eqtr3di  2282  eqtr4di  2285  eqtr4id  2286  eqeltrri  2308  eleqtrri  2310  eqeltrrid  2322  eleqtrrdi  2328  abid2  2357  abid2f  2412  eqnetrri  2439  neeqtrri  2443  eqsstrri  3275  sseqtrri  3277  eqsstrrid  3289  sseqtrrdi  3291  difdif2ss  3482  inrab2  3498  dfopg  3886  opid  3906  eqbrtrri  4137  breqtrri  4141  breqtrrdi  4156  opwo0id  4370  pwin  4408  limon  4640  tfis  4710  dfdm2  5302  cnvresid  5435  fores  5605  funcoeqres  5650  f1oprg  5665  fvmbr  5710  fnmptfvd  5787  funopdmsn  5869  fmptpr  5881  fsnunres  5891  idref  5935  riotaeqimp  6036  riotaprop  6037  fo1st  6364  fo2nd  6365  fnmpoovd  6424  ixpsnf1o  6984  phplem4  7122  snnen2og  7126  phplem4on  7135  pw1dc0el  7184  ss1o0el1o  7186  sbthlemi5  7244  eldju  7372  casefun  7389  omp1eomlem  7398  exmidfodomrlemim  7517  caucvgsrlembound  8125  ax0id  8209  1p1e2  9374  1e2m1  9376  2p1e3  9391  3p1e4  9393  4p1e5  9394  5p1e6  9395  6p1e7  9396  7p1e8  9397  8p1e9  9398  div4p1lem1div2  9512  0mnnnnn0  9548  zeo  9704  num0u  9740  numsucc  9769  decsucc  9770  1e0p1  9771  nummac  9774  decsubi  9792  decmul1  9793  decmul10add  9798  6p5lem  9799  10m1e9  9825  5t5e25  9832  6t6e36  9837  8t6e48  9848  decbin3  9871  infrenegsupex  9947  ige3m2fz  10406  fseq1p1m1  10453  fz0tp  10481  fz0to4untppr  10483  1fv  10498  fzo0to42pr  10590  fzosplitpr  10604  fzosplitprm1  10605  fldiv4lem1div2uz2  10693  xnn0nnen  10826  expnegap0  10936  sq4e2t8  11026  3dec  11104  fihashen1  11190  pr0hash2ex  11208  fundm2domnop0  11248  pfxccat3  11454  swrdccat  11455  pfxccatpfx2  11457  swrdccat3blem  11459  swrdccat3b  11460  cats2catd  11489  imi  11614  infxrnegsupex  11977  zsumdc  12099  fsumadd  12121  hashrabrex  12196  ntrivcvgap  12263  fprodmul  12306  fproddivapf  12346  fprodmodd  12356  efsep  12406  3dvds  12579  3dvdsdec  12580  3dvds2dec  12581  flodddiv4  12651  lcmneg  12800  dec2dvds  13138  2exp5  13159  2exp11  13163  ballotfilemth  13229  ennnfonelem1  13246  nninfdclemp1  13289  ndxid  13324  2strstr1g  13423  srgfcl  14220  isrhm  14407  issubrng  14449  rmodislmod  14629  cnfld0  14849  cnfld1  14850  cnfldplusf  14852  cnfldui  14867  toponrestid  15016  istpsi  15034  distopon  15082  distps  15086  discld  15131  txbas  15253  txdis  15272  txdis1cn  15273  txhmeo  15314  txswaphmeolem  15315  dvmptidcn  15709  dvmptid  15711  sinq34lt0t  15826  loge  15862  2logb9irr  15966  2logb9irrALT  15969  sqrt2cxp2logb9e3  15970  2logb9irrap  15972  lgsdir  16038  2lgslem3a  16096  2lgslem3b  16097  2lgslem3c  16098  2lgslem3d  16099  2lgslem3d1  16103  2lgsoddprmlem3d  16113  2sqlem9  16127  2sqlem10  16128  setsvtx  16176  edgiedgbg  16190  edg0iedg0g  16191  isuhgrm  16196  isushgrm  16197  uhgr0  16210  isupgren  16220  isumgren  16230  umgrpredgv  16272  isuspgren  16282  isusgren  16283  ausgrusgrben  16293  usgrf1oedg  16330  uhgr2edg  16331  usgredg3  16339  ushgredgedg  16351  ushgredgedgloop  16353  usgr0  16364  egrsubgr  16388  0grsubgr  16389  vtxdfifiun  16422  edginwlkd  16480  wlk1walkdom  16484  clwwlknon2x  16560  clwwlknonex2lem1  16562  konigsberglem1  16613  konigsberglem2  16614  konigsberglem3  16615  konigsberglem5  16617  ex-ceil  16624  ex-gcd  16629  bj-charfundcALT  16719  bdceqir  16754  bj-ssom  16846  trilpolemgt1  16963  redcwlpolemeq1  16979