Theorem eqcomd 2244

Description: Deduction from commutative law for class equality. (Contributed by NM, 15-Aug-1994.)

Hypothesis

Ref	Expression
eqcomd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eqcomd	⊢ (𝜑 → 𝐵 = 𝐴)

Proof of Theorem eqcomd

Step	Hyp	Ref	Expression
1		eqcomd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqcom 2240	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
3	1, 2	sylib 122	1 ⊢ (𝜑 → 𝐵 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = 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:  eqtr2d  2272  eqtr3d  2273  eqtr4d  2274  eqtr2id  2284  eqtr2di  2288  sylan9req  2292  eqeltrrd  2316  eleqtrrd  2318  eleqtrrid  2328  eqeltrrdi  2330  eqabcdv  2370  eqnetrrd  2446  neeqtrrd  2450  rspcedeq2vd  2940  dedhb  2995  eqsstrrd  3285  sseqtrrd  3287  eqsstrrdi  3301  dfrab3ss  3511  uneqdifeqim  3613  ifbothdadc  3674  ifbothdc  3675  2if2dc  3680  ifeqeqxdc  3687  disjsn2  3772  diftpsn3  3856  elpr2elpr  3901  dfopg  3902  unimax  3969  sndisj  4126  eqbrtrrd  4155  breqtrrd  4159  breqtrrid  4169  eqbrtrrdi  4171  class2seteq  4302  opth1  4378  euotd  4397  opelopabsb  4404  tfisi  4736  0nelxp  4804  opeliunxp  4832  euiotaex  5357  iota4  5360  iotam  5372  fun2ssres  5424  funimass1  5461  funssfv  5724  fnimapr  5766  fvun1  5772  fvco4  5780  elfvmptrab  5805  fmptco  5877  fncofn  5896  foima2  5960  foeqcnvco  5999  f1eqcocnv  6000  f1oiso2  6036  riotass2  6070  riotass  6071  f1ocnvfv3  6077  fvmpopr2d  6228  caovlem2d  6285  f1opw2  6299  offveq  6327  sbcopeq1a  6425  csbopeq1a  6426  eloprabi  6436  cnvf1olem  6464  f2ndf  6466  suppval1  6483  suppsnopdc  6494  smoiso  6577  nnaword  6788  eqer  6843  uniqs  6871  mapsncnv  6982  ixpiinm  7011  mapsnf1o  7024  mapunen  7156  ssenen  7157  findcard2  7198  findcard2s  7199  unsnfidcex  7232  fisseneq  7247  phpeqd  7248  en1eqsn  7271  sbthlemi6  7285  updjud  7429  omp1eomlem  7441  nnnninf2  7474  nninfisollem0  7477  nninfisollemeq  7479  fodju0  7494  3nsssucpw1  7602  enq0sym  7806  enq0tr  7808  recexgt0sr  8147  caucvgsrlemoffcau  8172  axcaucvglemval  8271  le2tri3i  8442  cnegexlem2  8510  nnpcan  8557  addlsub  8704  negf1o  8717  subdi  8720  rereim  8923  cru  8939  divmulassap  9034  divmulasscomap  9035  divap1d  9140  subhalfhalf  9552  div4p1lem1div2  9571  difgtsumgt  9726  elz2  9728  zindd  9776  qapne  10056  divge1  10142  xrlttri3  10217  fseq1p1m1  10519  fzrevral  10530  nn0disj  10563  fzo0addel  10624  fzosplitsnm1  10645  fzosplitprm1  10671  flqlelt  10730  flaplelt  10731  divfl0  10753  flqpmodeq  10786  zmodidfzo  10812  modqmuladd  10825  qnegmod  10828  addmodid  10831  modifeq2int  10845  modqeqmodmin  10853  modfzo0difsn  10854  modsumfzodifsn  10855  addmodlteq  10857  frecuzrdgsuc  10873  frecfzen2  10886  iseqf1olemab  10961  iseqf1olemmo  10964  seqf1oglem1  10978  seqf1oglem2  10979  ser3sub  10982  expgt1  11036  leexp2r  11052  sqoddm1div8  11153  mulsubdivbinom2ap  11172  bcm1k  11221  bcn2m1  11231  hashinfuni  11239  hashennnuni  11241  hashennn  11242  hashunlem  11267  hashprg  11272  fihashssdif  11282  hashfibclem  11305  hashfibc  11306  hashf1lem1  11308  hashf1lem2  11309  zfz1isolem1  11315  elovmpowrd  11369  ccatsymb  11393  ccatlid  11397  eqs1  11419  ccatw2s1p1g  11436  swrdfv2  11458  swrds1  11463  swrdlsw  11464  pfxfv  11479  swrdswrd  11500  swrdpfx  11502  pfxpfx  11503  pfxlswccat  11508  ccats1pfxeq  11509  wrdind  11517  wrd2ind  11518  pfxccatin12lem1  11523  pfxccatin12lem2  11526  swrdccat3blem  11534  swrdccat3b  11535  ccats1pfxeqbi  11537  reuccatpfxs1lem  11541  reuccatpfxs1  11542  s3s4d  11598  s2s5d  11599  s5s2d  11600  shftlem  11604  shftfvalg  11606  shftfval  11609  replim  11647  cjexp  11681  sq01  11683  resqrexlemcalc1  11803  resqrexlemcvg  11808  rersqrtthlem  11819  abssq  11871  recan  11899  negfi  12018  minclpr  12028  mingeb  12034  xrmaxiflemcom  12041  xrmineqinf  12061  xrminltinf  12064  xrminadd  12067  climmpt  12092  climrecl  12116  fsum3cvg  12171  summodclem3  12173  summodclem2a  12174  modfsummodlemstep  12250  isumsplit  12284  arisum  12291  geosergap  12299  geo2sum  12307  mertenslemi1  12328  mertenslem2  12329  clim2divap  12333  fproddccvg  12365  fprodssdc  12383  fprodabs  12409  fproddivapf  12424  fprodmodd  12434  efcj  12466  efsub  12474  eflegeo  12494  sinneg  12519  cosneg  12520  sin01bnd  12550  cos01bnd  12551  modm1div  12593  summodnegmod  12615  dvdseq  12641  addmodlteqALT  12652  mulmoddvds  12656  zob  12684  nn0ob  12701  divalgmod  12720  flodddiv4  12729  bitsinv1  12755  divgcdnnr  12779  gcdneg  12785  bezoutlemsup  12812  dvdssq  12834  lcmneg  12878  3lcm2e6woprm  12890  6lcm4e12  12891  divgcdcoprmex  12906  cncongr1  12907  cncongrcoprm  12910  nnmaxpwlemxy  12974  nnmaxpwlemnfac  12977  divnumden  13002  zgcdsq  13007  phibnd  13025  hashgcdlem  13046  vfermltl  13060  powm2modprm  13061  reumodprminv  13062  pythagtriplem19  13091  pcprendvds2  13100  pczpre  13106  dvdsprmpweqle  13146  difsqpwdvds  13147  4sqlem4  13201  prmlem0  13250  ballotfilemfp1  13290  ballotfilemsf1o  13316  ballotfilemrinv0  13335  ennnfonelemex  13364  strndxid  13439  topnvalg  13665  intopsn  13747  ismgmid2  13760  mgmidsssn0  13764  gzsumfzval  13771  mndpfo  13811  mndfo  13812  mndinvmod  13818  mnd1id  13823  mhmf1o  13837  0mhm  13853  gzsumwmhm  13863  grpidd2  13906  grpinvid2  13918  grpidssd  13941  grpnpcan  13957  grpsubsub4  13958  qusgrp2  13976  mulginvcom  14010  grpissubg  14057  quselbasg  14093  qus0  14098  ecqusaddd  14101  ghmid  14112  ghminv  14113  cntrval  14152  imasabl  14231  gzsummhm  14236  gzsumsplit0  14239  gzsumshift  14240  gsumsncmn  14247  gsumcom2fi  14276  prdssca  14283  prds0g  14303  mgpress  14338  rnglz  14352  rngrz  14353  rngmneg1  14354  rngmneg2  14355  rngpropd  14362  rng1zrlem  14366  srgmulgass  14401  srgpcomp  14402  srgpcomppsc  14404  ringadd2  14440  ringo2times  14441  ringlz  14456  ringrz  14457  ringinvnzdiv  14463  ringnegl  14464  ringnegr  14465  imasring  14479  qusring2  14481  crngunit  14528  rhmopp  14593  lringuplu  14613  opprdomnbg  14693  lmod0vs  14768  lmodvsmmulgdi  14770  lmodfopne  14773  islss3  14826  lspsn  14863  lmodindp1  14875  rnglidlmmgm  14943  rnglidlmsgrp  14944  rnglidlrng  14945  isridl  14951  zringinvg  15049  zndvds  15094  znf1o  15096  assa2ass  15119  assa2ass2  15120  asclinvg  15142  assamulgscmlem1  15151  assamulgscmlem2  15152  psrgrp  15200  toponcom  15265  tgtopon  15304  restopnb  15419  cnptoprest  15477  blfvalps  15623  bdmopn  15742  cnmet  15768  mpomulcn  15804  limcdifap  15900  dvidsslem  15931  dviaddf  15943  dvexp  15949  dvply2g  16004  coseq0negpitopi  16075  abssinper  16085  rplogbzexp  16202  pellexlem2  16242  dvdsppwf1o  16295  mpodvdsmulf1o  16296  fsumdvdsmul  16297  sgmmul  16302  perfect  16313  bcmono  16316  prmefexple  16320  bposlem1  16323  bposlem9  16331  lgsvalmod  16355  lgsneg  16360  gausslemma2dlem1a  16394  gausslemma2dlem6  16403  gausslemma2dlem7  16404  gausslemma2d  16405  lgsquadlem2  16414  2lgslem1a1  16422  2lgslem1a  16424  2lgslem3c  16431  2lgslem3d  16432  2lgslem3d1  16436  2lgs  16440  2lgsoddprm  16449  uhgrun  16544  upgrun  16584  umgrun  16586  ushgredgedg  16684  issubgr2  16716  uhgrissubgr  16719  subgruhgredgdm  16728  subumgredg2en  16729  subupgr  16731  p1evtxdeqfilem  16769  wlklenvm1  16799  wlklenvm1g  16800  wlkl1loop  16816  upgriswlkdc  16818  uspgr2wlkeq  16823  uspgr2wlkeq2  16824  uspgr2wlkeqi  16825  wlkres  16837  loopclwwlkn1b  16877  clwwlkn1loopb  16878  clwwlkext2edg  16880  clwwlknonccat  16891  s2elclwwlknon2  16894  clwwlknonex2lem2  16896  clwwlknun  16899  eupth2lem3fi  16934  eupth2lembfi  16935  subctctexmid  17247  cvgcmp2nlemabs  17299  trilpolemlt1  17309