Theorem eqcom 2828

Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Assertion

Ref	Expression
eqcom	⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Proof of Theorem eqcom

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	eqcomd 2827	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2827	. 2 ⊢ (𝐵 = 𝐴 → 𝐴 = 𝐵)
5	2, 4	impbii 211	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 208   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  eqcoms  2829  eqcomi  2830  neqcomd  2831  eqeq2d  2832  eqtr2  2842  eqtr3  2843  abeq1  2946  necom  3069  nesym  3072  pm13.181  3099  gencbvex  3549  clel5  3656  eqsbc3r  3836  dfss  3952  sspsstri  4078  ssnelpss  4087  ssdifim  4238  disj4  4407  reuprg0  4631  preq1b  4770  invdisj  5042  disjprgw  5053  disjprg  5054  dtruALT  5280  reusv3  5297  dtruALT2  5327  opthg2  5363  copsex4g  5377  opcom  5383  opeqsng  5385  opeqpr  5387  snopeqop  5388  propeqop  5389  opthwiener  5396  opthprc  5610  elxp3  5612  relop  5715  dmopab3  5782  rncoeq  5840  restidsing  5916  somin1  5987  xpcan  6027  xpcan2  6028  dfrel4v  6041  dmsnn0  6058  reu3op  6137  reuop  6138  opreu2reurex  6139  ordtri2  6220  ordtri2or3  6282  suc11  6288  on0eqel  6302  snsn0non  6303  iota1  6326  iotan0  6339  sniota  6340  mptfnf  6477  fresaunres1  6545  dffn5  6718  fvelrnb  6720  dfimafn2  6723  funimass4  6724  feqmptdf  6729  fnsnfv  6737  dmfco  6751  fndmdif  6806  fneqeql  6810  rexrn  6847  ralrn  6848  elrnrexdmb  6850  dffo4  6863  funopsn  6904  ftpg  6912  fprb  6950  rexima  6993  ralima  6994  fvclss  6995  dff13  7007  f1eqcocnv  7051  riotaeqimp  7134  eusvobj2  7143  f1ocnvfv3  7146  oprabidw  7181  oprabid  7182  oprabv  7208  eloprabga  7255  ovelimab  7320  onmindif2  7521  br1steqg  7705  br2ndeqg  7706  dfoprab3  7746  opiota  7751  f1o2ndf1  7812  brtpos2  7892  tpossym  7918  mpocurryd  7929  rdglim2  8062  tz7.48lem  8071  oaf1o  8183  omopthi  8278  erth2  8333  brecop  8384  erovlem  8387  ecopovsym  8393  eceqoveq  8396  xpcomco  8601  omxpenlem  8612  mapen  8675  nneneq  8694  unxpdomlem3  8718  unfilem1  8776  mapfien  8865  supgtoreq  8928  wemapsolem  9008  suc11reg  9076  inf3lem2  9086  inf3lem6  9090  djulf1o  9335  djurf1o  9336  infenaleph  9511  isinfcard  9512  dfac5  9548  cfeq0  9672  cfsuc  9673  ssfin4  9726  fin23lem25  9740  fin23lem22  9743  fin23lem40  9767  fin1a2lem5  9820  axcclem  9873  brdom7disj  9947  brdom6disj  9948  inar1  10191  psslinpr  10447  ltexprlem4  10455  ltsrpr  10493  mulgt0sr  10521  elreal  10547  ltresr  10556  leloe  10721  eqlei2  10745  addsubeq4  10895  subcan2  10905  negcon1  10932  negcon2  10933  addid0  11053  addeq0  11057  divmul2  11296  conjmul  11351  rereccl  11352  creur  11626  creui  11627  nndiv  11677  nn0sub  11941  elnn0z  11988  elznn0  11990  xrleloe  12531  ngtmnft  12553  icoshftf1o  12854  iccf1o  12876  fzen  12918  fzneuz  12982  injresinj  13152  fleqceilz  13216  mod0  13238  modmuladdnn0  13277  modirr  13304  addmodlteq  13308  nn0ennn  13341  hashrabsn01  13728  hashsdom  13736  hashgt12el2  13778  hashbclem  13804  hashfacen  13806  hashf1lem1  13807  hashtpg  13837  fi1uzind  13849  ccatw2s1p1  13989  ccatw2s1p1OLD  13990  wrd2ind  14079  cshw1  14178  scshwfzeqfzo  14182  s2f1o  14272  wwlktovfo  14316  dmtrclfv  14372  cjreb  14476  leabs  14653  reusq0  14816  incexc2  15187  pwm1geoserOLD  15219  rpnnen2lem12  15572  dvdsval2  15604  dvdsabseq  15657  dvdsflip  15661  odd2np1  15684  oddm1even  15686  sqoddm1div8z  15697  m1exp1  15721  divalglem4  15741  divalglem8  15745  divalgb  15749  modremain  15753  zeqzmulgcd  15853  dfgcd2  15888  lcmfpr  15965  lcmftp  15974  lcmfunsnlem2  15978  divgcdcoprm0  16003  prm2orodd  16029  hashdvds  16106  oddprmdvds  16233  vdwlem12  16322  cshwshashlem1  16423  cshwsiun  16427  initoid  17259  termoid  17260  setcinv  17344  yonedainv  17525  joinfval  17605  joinfval2  17606  meetfval  17619  meetfval2  17620  latnle  17689  sgrp2nmndlem3  18084  grpid  18133  grpinvcnv  18161  grplmulf1o  18167  grpsubeq0  18179  grpsubadd  18181  grplactcnv  18196  isnsg4  18313  cycsubmel  18337  conjghm  18383  conjnmzb  18387  gacan  18429  gapm  18430  cntzrec  18458  oppgcntz  18486  fvcosymgeq  18551  odmulgeq  18678  dfod2  18685  sylow3lem3  18748  sylow3lem6  18751  lssnle  18794  lsmhash  18825  efgredlemb  18866  efgrelexlemb  18870  dprd2d2  19160  ablfac1eulem  19188  pgpfac1lem2  19191  pgpfac1lem4  19194  dvdsrval  19389  dvdsr02  19400  rmodislmodlem  19695  lvecinv  19879  rspsn  20021  0ring01eqbi  20040  psrbagconf1o  20148  mplmonmul  20239  gsummoncoe1  20466  prmirredlem  20634  zndvds  20690  znleval  20695  mat1dimelbas  21074  mat1dimbas  21075  1mavmul  21151  ma1repveval  21174  mulmarep1gsum1  21176  mdetunilem9  21223  m2cpminvid2lem  21356  pmatcollpw3lem  21385  mp2pm2mplem4  21411  toponsspwpw  21524  dmtopon  21525  cmpfi  22010  ssref  22114  qtopeu  22318  hmeoimaf1o  22372  txhmeo  22405  fbasrn  22486  rnelfmlem  22554  hauspwpwf1  22589  alexsubALTlem4  22652  qustgpopn  22722  qustgphaus  22725  fmucndlem  22894  isngp3  23201  isngp4  23215  metnrmlem1a  23460  icopnfcnv  23540  iccpnfcnv  23542  ivthle  24051  ivthle2  24052  dyadmbl  24195  mbfinf  24260  i1fmulclem  24297  itg1mulc  24299  mvth  24583  dvivth  24601  lhop2  24606  dvdsq1p  24748  reeff1o  25029  coseq1  25104  recosf1o  25113  resinf1o  25114  efopn  25235  cxpeq  25332  logreclem  25334  affineequiv  25395  affineequiv4  25398  affineequivne  25399  quad2  25411  dcubic  25418  mcubic  25419  quart  25433  atandm2  25449  rlimcnp2  25538  amgm  25562  wilthlem2  25640  mumullem2  25751  sqff1o  25753  dvdsflf1o  25758  gausslemma2dlem0i  25934  lgseisenlem2  25946  lgsquadlem2  25951  2lgslem1c  25963  2lgsoddprmlem2  25979  2lgsoddprm  25986  2sq2  26003  addsq2reu  26010  2sqreultlem  26017  2sqreunnltlem  26020  2sqreulem3  26023  tgjustf  26253  legtrid  26371  legso  26379  islmib  26567  lmicom  26568  lmiinv  26572  lmimid  26574  lmiopp  26582  colinearalglem2  26687  colinearalg  26690  ax5seglem4  26712  ax5seglem5  26713  axlowdimlem13  26734  axeuclidlem  26742  axeuclid  26743  axcontlem2  26745  axcontlem4  26747  elntg2  26765  structiedg0val  26801  usgredgsscusgredg  27235  fusgrn0degnn0  27275  umgr2v2evtxel  27298  vdiscusgrb  27306  uspgr2wlkeq  27421  wlk0prc  27429  wlklenvclwlk  27430  wlklenvclwlkOLD  27431  wlkp1lem8  27456  spthdep  27509  usgr2pthlem  27538  usgr2pth  27539  wlkiswwlksupgr2  27649  wlklnwwlkln2lem  27654  wwlksnextproplem3  27684  umgr2adedgwlk  27718  umgr2adedgspth  27721  umgr2wlkon  27723  umgrwwlks2on  27730  elwwlks2  27739  elwspths2spth  27740  clwlkclwwlklem2a4  27769  clwlkclwwlklem2  27772  erclwwlkref  27792  clwwlkf  27820  erclwwlknref  27842  erclwwlknsym  27843  erclwwlkntr  27844  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  eupth2lem2  27992  eucrct2eupth  28018  numclwwlkqhash  28148  isgrpo  28268  hvsubaddi  28837  hire  28865  shmodsi  29160  omlsilem  29173  chcon1i  29236  chnlei  29256  pjoml3i  29357  cmbr2i  29367  chscllem2  29409  adjsym  29604  eigorthi  29608  dfadj2  29656  adjval2  29662  cnvadj  29663  dmadjrnb  29677  adjvalval  29708  cnlnadjeui  29848  cnlnssadj  29851  adjbdln  29854  pjimai  29947  pjin2i  29964  pjin3i  29965  stadd3i  30019  largei  30038  cvnbtwn3  30059  cvnbtwn4  30060  mddmd2  30080  superpos  30125  atnemeq0  30148  sumdmdii  30186  sumdmdlem  30189  addltmulALT  30217  opreu2reuALT  30234  foresf1o  30259  difeq  30274  disjrdx  30335  fcoinvbr  30352  fmptco1f1o  30372  dfimafnf  30375  funcnvmpt  30406  curry2ima  30438  cnvoprabOLD  30450  elicoelioo  30495  wrdt2ind  30622  swrdrn3  30624  orngsqr  30872  qusker  30913  eqg0el  30921  lsmsnorb  30940  xrmulc1cn  31168  xrge0iifcnv  31171  ind1a  31273  esumfsup  31324  esumpcvgval  31332  esumcvg  31340  esum2dlem  31346  issgon  31377  eulerpartgbij  31625  eulerpartlemgh  31631  ballotlemsima  31768  bnj1366  32096  bnj553  32165  bnj964  32210  cusgredgex  32363  revwlk  32366  loop1cycl  32379  subfacp1lem3  32424  subfacp1lem5  32426  erdszelem9  32441  prv1n  32673  quad3  32908  br6  32988  elintfv  33002  dfon2lem5  33027  dfon2lem8  33030  soseq  33091  sltval2  33158  sltintdifex  33163  sltres  33164  nosepon  33167  noextenddif  33170  nosepssdm  33185  nosupno  33198  sleloe  33228  scutbdaylt  33271  brbigcup  33354  dfbigcup2  33355  elfix  33359  ellimits  33366  snelsingles  33378  dfiota3  33379  imageval  33386  brapply  33394  brsuccf  33397  funpartlem  33398  brfullfun  33404  dfrecs2  33406  dfrdg4  33407  altopthbg  33424  altopthc  33427  altopthd  33428  altopelaltxp  33432  brsegle  33564  outsideofrflx  33583  elicc3  33660  nn0prpw  33666  opnregcld  33673  cldregopn  33674  fneval  33695  topfneec  33698  knoppndvlem9  33854  bj-elsngl  34275  bj-snglc  34276  bj-projval  34303  bj-disj2r  34335  bj-restreg  34384  bj-0int  34387  copsex2b  34426  bj-inftyexpitaudisj  34481  bj-inftyexpidisj  34486  bj-isrvec  34569  bj-bary1lem1  34586  topdifinffinlem  34622  topdifinfeq  34625  fvineqsnf1  34685  curf  34864  uncf  34865  curunc  34868  unccur  34869  poimirlem2  34888  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem20  34906  poimirlem27  34913  mblfinlem2  34924  mbfresfi  34932  itg2addnclem2  34938  ftc1anclem3  34963  fdc  35014  heibor1  35082  opidonOLD  35124  0rngo  35299  smprngopr  35324  isfldidl  35340  isfldidl2  35341  eqelb  35496  ideq2  35559  relcnveq  35573  n0elqs  35577  elrelscnveq  35726  lcvnbtwn3  36158  lcvexchlem1  36164  lsatnem0  36175  opcon1b  36328  omllaw2N  36374  cmtbr2N  36383  leatb  36422  cvlsupr2  36473  glbconxN  36508  islln3  36640  llnexatN  36651  islpln3  36663  lplnexatN  36693  islvol3  36706  dalem-cly  36801  isline4N  36907  2llnma3r  36918  poml4N  37083  4atex2  37207  4atex2-0bOLDN  37209  cdlemefrs29bpre0  37526  cdlemftr3  37695  cdlemb3  37736  cdlemg17h  37798  cdlemg17pq  37802  cdlemg19  37814  cdlemg21  37816  tendoex  38105  dva1dim  38115  dihglb2  38472  doch11  38503  dochsordN  38504  lcfrlem9  38680  hlhillcs  39088  addsubeq4com  39159  elrfirn  39285  isnacs2  39296  isnacs3  39300  fiphp3d  39409  wopprc  39620  islnm2  39671  kercvrlsm  39676  fgraphopab  39803  rp-fakeuninass  39875  snen1g  39883  iscard4  39893  frege124d  40099  frege129d  40101  frege92  40294  dffrege99  40301  clsk3nimkb  40383  clsk1indlem4  40387  clsk1indlem1  40388  ntrclsiso  40410  ntrclsk3  40413  ntrclsk13  40414  ntrneik4w  40443  extoimad  40508  int-sqdefd  40527  int-sqgeq0d  40532  radcnvrat  40639  bcc0  40665  opelopab4  40878  eqsbc3rVD  41167  fzisoeu  41560  iuneqfzuz  41596  supxrleubrnmptf  41720  fsummulc1f  41844  fsumiunss  41849  fmul01lt1lem2  41859  sumnnodd  41904  fnlimfvre2  41951  limsupreuz  42011  limsupvaluz2  42012  liminfvalxr  42057  icccncfext  42163  cncfiooicc  42170  cncfioobdlem  42172  dvmptmulf  42215  dvmptfprodlem  42222  volioc  42250  itgioocnicc  42255  fourierdlem12  42398  fourierdlem20  42406  fourierdlem25  42411  fourierdlem33  42419  fourierdlem42  42428  fourierdlem52  42437  fourierdlem54  42439  fourierdlem57  42442  fourierdlem58  42443  fourierdlem59  42444  fourierdlem63  42448  fourierdlem65  42450  fourierdlem68  42453  fourierdlem73  42458  fourierdlem74  42459  fourierdlem75  42460  fourierdlem80  42465  fourierdlem81  42466  rrndistlt  42569  sge0ltfirpmpt2  42702  sge0pnfmpt  42721  hoidmv1le  42870  hoidmvle  42876  vonioolem2  42957  smflimlem3  43043  euabsneu  43257  funressnfv  43272  aiotaval  43287  reuf1odnf  43300  reuf1od  43301  afvpcfv0  43339  dfafn5a  43353  afvelrnb  43356  afvelrnb0  43357  dfaimafn2  43359  dfatsnafv2  43445  dfatdmfcoafv2  43447  f1oresf1o2  43484  0nelsetpreimafv  43544  fargshiftfo  43596  sprsymrelf1  43652  reupr  43678  fmtnorec2lem  43698  fmtnoprmfac1  43721  fmtnoprmfac2  43723  sfprmdvdsmersenne  43762  lighneallem2  43765  dfeven2  43808  dfodd3  43809  odd2np1ALTV  43833  even3prm2  43878  fppr2odd  43890  nnsum3primesgbe  43951  nnsum3primesle9  43953  isomuspgrlem2d  43990  0nodd  44071  2nodd  44073  lmod0rng  44133  rngcinv  44246  rngcinvALTV  44258  ringcinv  44297  ringcinvALTV  44321  lcoel0  44477  lindslinindimp2lem4  44510  ldepspr  44522  lincresunit3  44530  nn0sumshdiglemB  44674  nn0sumshdiglem1  44675  rrx2pnedifcoorneorr  44698  eenglngeehlnmlem1  44718  eenglngeehlnmlem2  44719  rrx2linest  44723  rrx2linest2  44725  rrxsphere  44729  line2ylem  44732  line2x  44735  itscnhlc0xyqsol  44746  itschlc0xyqsol1  44747  itsclinecirc0b  44755  2itscp  44762  inlinecirc02plem  44767