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  4154  breqtrrd  4158  breqtrrid  4168  eqbrtrrdi  4170  class2seteq  4300  opth1  4376  euotd  4395  opelopabsb  4402  tfisi  4734  0nelxp  4802  opeliunxp  4830  euiotaex  5354  iota4  5357  iotam  5369  fun2ssres  5421  funimass1  5458  funssfv  5721  fnimapr  5763  fvun1  5769  fvco4  5777  elfvmptrab  5802  fmptco  5874  fncofn  5893  foima2  5957  foeqcnvco  5996  f1eqcocnv  5997  f1oiso2  6033  riotass2  6067  riotass  6068  f1ocnvfv3  6074  fvmpopr2d  6225  caovlem2d  6282  f1opw2  6296  offveq  6323  sbcopeq1a  6421  csbopeq1a  6422  eloprabi  6432  cnvf1olem  6460  f2ndf  6462  suppval1  6479  suppsnopdc  6490  smoiso  6573  nnaword  6784  eqer  6839  uniqs  6867  mapsncnv  6977  ixpiinm  7006  mapsnf1o  7019  mapunen  7151  ssenen  7152  findcard2  7193  findcard2s  7194  unsnfidcex  7227  fisseneq  7242  phpeqd  7243  en1eqsn  7265  sbthlemi6  7279  updjud  7422  omp1eomlem  7434  nnnninf2  7467  nninfisollem0  7470  nninfisollemeq  7472  fodju0  7487  3nsssucpw1  7595  enq0sym  7799  enq0tr  7801  recexgt0sr  8140  caucvgsrlemoffcau  8165  axcaucvglemval  8264  le2tri3i  8434  cnegexlem2  8502  nnpcan  8549  addlsub  8696  negf1o  8709  subdi  8712  rereim  8915  cru  8931  divmulassap  9026  divmulasscomap  9027  divap1d  9132  subhalfhalf  9542  div4p1lem1div2  9561  difgtsumgt  9716  elz2  9718  zindd  9766  qapne  10041  divge1  10126  xrlttri3  10201  fseq1p1m1  10503  fzrevral  10514  nn0disj  10547  fzo0addel  10608  fzosplitsnm1  10629  fzosplitprm1  10655  flqlelt  10713  divfl0  10733  flqpmodeq  10766  zmodidfzo  10792  modqmuladd  10805  qnegmod  10808  addmodid  10811  modifeq2int  10825  modqeqmodmin  10833  modfzo0difsn  10834  modsumfzodifsn  10835  addmodlteq  10837  frecuzrdgsuc  10853  frecfzen2  10866  iseqf1olemab  10941  iseqf1olemmo  10944  seqf1oglem1  10958  seqf1oglem2  10959  ser3sub  10962  expgt1  11016  leexp2r  11032  sqoddm1div8  11133  mulsubdivbinom2ap  11151  bcm1k  11200  bcn2m1  11210  hashinfuni  11218  hashennnuni  11220  hashennn  11221  hashunlem  11246  hashprg  11251  fihashssdif  11261  hashfibclem  11284  hashfibc  11285  hashf1lem1  11287  hashf1lem2  11288  zfz1isolem1  11294  elovmpowrd  11348  ccatsymb  11372  ccatlid  11376  eqs1  11398  ccatw2s1p1g  11415  swrdfv2  11437  swrds1  11442  swrdlsw  11443  pfxfv  11458  swrdswrd  11479  swrdpfx  11481  pfxpfx  11482  pfxlswccat  11487  ccats1pfxeq  11488  wrdind  11496  wrd2ind  11497  pfxccatin12lem1  11502  pfxccatin12lem2  11505  swrdccat3blem  11513  swrdccat3b  11514  ccats1pfxeqbi  11516  reuccatpfxs1lem  11520  reuccatpfxs1  11521  s3s4d  11577  s2s5d  11578  s5s2d  11579  shftlem  11583  shftfvalg  11585  shftfval  11588  replim  11626  cjexp  11660  sq01  11662  resqrexlemcalc1  11782  resqrexlemcvg  11787  rersqrtthlem  11798  abssq  11849  recan  11877  negfi  11996  minclpr  12005  mingeb  12010  xrmaxiflemcom  12017  xrmineqinf  12037  xrminltinf  12040  xrminadd  12043  climmpt  12068  climrecl  12092  fsum3cvg  12147  summodclem3  12149  summodclem2a  12150  modfsummodlemstep  12226  isumsplit  12260  arisum  12267  geosergap  12275  geo2sum  12283  mertenslemi1  12304  mertenslem2  12305  clim2divap  12309  fproddccvg  12341  fprodssdc  12359  fprodabs  12385  fproddivapf  12400  fprodmodd  12410  efcj  12442  efsub  12450  eflegeo  12470  sinneg  12495  cosneg  12496  sin01bnd  12526  cos01bnd  12527  modm1div  12569  summodnegmod  12591  dvdseq  12617  addmodlteqALT  12628  mulmoddvds  12632  zob  12660  nn0ob  12677  divalgmod  12696  flodddiv4  12705  bitsinv1  12731  divgcdnnr  12755  gcdneg  12761  bezoutlemsup  12788  dvdssq  12810  lcmneg  12854  3lcm2e6woprm  12866  6lcm4e12  12867  divgcdcoprmex  12882  cncongr1  12883  cncongrcoprm  12886  oddpwdclemxy  12949  oddpwdclemodd  12952  divnumden  12976  zgcdsq  12981  phibnd  12997  hashgcdlem  13018  vfermltl  13032  powm2modprm  13033  reumodprminv  13034  pythagtriplem19  13063  pcprendvds2  13072  pczpre  13078  dvdsprmpweqle  13118  difsqpwdvds  13119  4sqlem4  13173  ballotfilemfp1  13233  ballotfilemsf1o  13259  ballotfilemrinv0  13278  ennnfonelemex  13307  strndxid  13382  topnvalg  13607  intopsn  13689  ismgmid2  13702  mgmidsssn0  13706  gzsumfzval  13713  mndpfo  13753  mndfo  13754  mndinvmod  13760  mnd1id  13765  mhmf1o  13779  0mhm  13795  gzsumwmhm  13805  grpidd2  13848  grpinvid2  13860  grpidssd  13883  grpnpcan  13899  grpsubsub4  13900  qusgrp2  13918  mulginvcom  13952  grpissubg  13999  quselbasg  14035  qus0  14040  ecqusaddd  14043  ghmid  14054  ghminv  14055  imasabl  14142  gzsummhm  14147  gzsumsplit0  14150  gzsumshift  14151  gsumsncmn  14158  prdssca  14177  prds0g  14197  mgpress  14232  rnglz  14246  rngrz  14247  rngmneg1  14248  rngmneg2  14249  rngpropd  14256  rng1zrlem  14260  srgmulgass  14295  srgpcomp  14296  srgpcomppsc  14298  ringadd2  14334  ringo2times  14335  ringlz  14350  ringrz  14351  ringinvnzdiv  14357  ringnegl  14358  ringnegr  14359  imasring  14371  qusring2  14373  crngunit  14420  rhmopp  14485  lringuplu  14505  opprdomnbg  14585  lmod0vs  14660  lmodvsmmulgdi  14662  lmodfopne  14665  islss3  14718  lspsn  14755  lmodindp1  14767  rnglidlmmgm  14835  rnglidlmsgrp  14836  rnglidlrng  14837  isridl  14843  zringinvg  14941  zndvds  14986  znf1o  14988  assa2ass  15011  assa2ass2  15012  asclinvg  15034  assamulgscmlem1  15043  assamulgscmlem2  15044  psrgrp  15078  toponcom  15130  tgtopon  15169  restopnb  15284  cnptoprest  15342  blfvalps  15488  bdmopn  15607  cnmet  15633  mpomulcn  15669  limcdifap  15765  dvidsslem  15796  dviaddf  15808  dvexp  15814  dvply2g  15869  coseq0negpitopi  15940  abssinper  15950  rplogbzexp  16062  pellexlem2  16098  dvdsppwf1o  16109  mpodvdsmulf1o  16110  fsumdvdsmul  16111  sgmmul  16116  perfect  16121  bcmono  16124  lgsvalmod  16150  lgsneg  16155  gausslemma2dlem1a  16189  gausslemma2dlem6  16198  gausslemma2dlem7  16199  gausslemma2d  16200  lgsquadlem2  16209  2lgslem1a1  16217  2lgslem1a  16219  2lgslem3c  16226  2lgslem3d  16227  2lgslem3d1  16231  2lgs  16235  2lgsoddprm  16244  uhgrun  16339  upgrun  16379  umgrun  16381  ushgredgedg  16479  issubgr2  16511  uhgrissubgr  16514  subgruhgredgdm  16523  subumgredg2en  16524  subupgr  16526  p1evtxdeqfilem  16564  wlklenvm1  16594  wlklenvm1g  16595  wlkl1loop  16611  upgriswlkdc  16613  uspgr2wlkeq  16618  uspgr2wlkeq2  16619  uspgr2wlkeqi  16620  wlkres  16632  loopclwwlkn1b  16672  clwwlkn1loopb  16673  clwwlkext2edg  16675  clwwlknonccat  16686  s2elclwwlknon2  16689  clwwlknonex2lem2  16691  clwwlknun  16694  eupth2lem3fi  16729  eupth2lembfi  16730  subctctexmid  17042  cvgcmp2nlemabs  17093  trilpolemlt1  17102