Theorem eqcom 2743

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 2742	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2742	. 2 ⊢ (𝐵 = 𝐴 → 𝐴 = 𝐵)
5	2, 4	impbii 209	1 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqcoms  2744  eqcomi  2745  neqcomd  2746  eqeq2d  2747  eqabcbw  2810  eqabcb  2876  necom  2985  nesym  2988  gencbvex  3487  clel5  3607  eqsbc2  3792  dfss  3908  sspsstri  4045  ssdifim  4213  disj4  4399  reuprg0  4646  preq1b  4789  invdisj  5071  disjprg  5081  dtruALT  5330  reusv3  5347  opthg2  5432  copsex2g  5447  copsex4g  5449  opcom  5455  opeqsng  5457  opeqpr  5459  snopeqop  5460  propeqop  5461  opthwiener  5468  vopelopabsb  5484  opthprc  5695  elxp3  5697  relop  5805  dmopab3  5874  rnopab3  5911  rncoeq  5937  restidsing  6018  somin1  6096  xpcan  6140  xpcan2  6141  dfrel4v  6154  dmsnn0  6171  reu3op  6256  reuop  6257  opreu2reurex  6258  ordtri2  6358  ordtri2or3  6425  suc11  6432  on0eqel  6448  snsn0non  6449  iota1  6477  iotan0  6488  sniota  6489  mptfnf  6633  fresaunres1  6713  dffn5  6898  fvelrnb  6900  dfimafn2  6903  funimass4  6904  feqmptdf  6910  fnsnfv  6919  dmfco  6936  funcnvmpt  6949  fndmdif  6994  fneqeql  6998  rexrn  7039  ralrn  7040  elrnrexdmb  7042  dffo4  7055  fssrescdmd  7079  funopsn  7101  funopsnOLD  7102  ftpg  7110  fprb  7149  ralima  7192  reximaOLD  7194  ralimaOLD  7195  fvclss  7196  dff13  7209  f1eqcocnv  7256  fnssintima  7317  imaeqsexvOLD  7318  riotaeqimp  7350  eusvobj2  7359  f1ocnvfv3  7362  oprabidw  7398  oprabid  7399  oprabv  7427  eloprabga  7476  ovelimab  7545  onmindif2  7761  br1steqg  7964  br2ndeqg  7965  dfoprab3  8007  opiota  8012  f1o2ndf1  8072  soseq  8109  brtpos2  8182  tpossym  8208  mpocurryd  8219  rdglim2  8371  tz7.48lem  8380  oaf1o  8498  omopthi  8597  erth2  8699  brecop  8757  erovlem  8760  ecopovsym  8766  eceqoveq  8769  xpcomco  9005  omxpenlem  9016  mapen  9079  nneneq  9140  unxpdomlem3  9168  unfilem1  9215  mapfien  9321  supgtoreq  9384  wemapsolem  9465  suc11reg  9540  inf3lem2  9550  inf3lem6  9554  ttrcltr  9637  djulf1o  9836  djurf1o  9837  infenaleph  10013  isinfcard  10014  dfac5  10051  cfeq0  10178  cfsuc  10179  ssfin4  10232  fin23lem25  10246  fin23lem22  10249  fin23lem40  10273  fin1a2lem5  10326  axcclem  10379  brdom7disj  10453  brdom6disj  10454  inar1  10698  psslinpr  10954  ltexprlem4  10962  ltsrpr  11000  mulgt0sr  11028  elreal  11054  ltresr  11063  leloe  11232  eqlei2  11257  addsubeq4  11408  subcan2  11419  negcon1  11446  negcon2  11447  addid0  11569  addeq0  11573  divmul2  11813  conjmul  11872  rereccl  11873  creur  12153  creui  12154  ind1a  12170  nndiv  12223  nn0sub  12487  elnn0z  12537  elznn0  12539  xrleloe  13095  ngtmnft  13118  icoshftf1o  13427  iccf1o  13449  fzen  13495  fzneuz  13562  injresinj  13746  fleqceilz  13813  mod0  13835  modmuladdnn0  13877  modirr  13904  addmodlteq  13908  nn0ennn  13941  hashrabsn01  14335  hashsdom  14343  hashgt12el2  14385  hashbclem  14414  hashfacen  14416  hashf1lem1  14417  hashtpg  14447  tpf1o  14463  fi1uzind  14469  ccatw2s1p1  14599  wrd2ind  14685  cshw1  14784  cshwsexa  14786  scshwfzeqfzo  14788  s2f1o  14878  wwlktovfo  14920  dmtrclfv  14980  cjreb  15085  leabs  15261  reusq0  15427  incexc2  15803  rpnnen2lem12  16192  dvdsval2  16224  dvdsabseq  16282  dvdsflip  16286  odd2np1  16310  oddm1even  16312  sqoddm1div8z  16323  m1exp1  16345  divalglem4  16365  divalglem8  16369  divalgb  16373  modremain  16377  zeqzmulgcd  16479  dfgcd2  16515  lcmfpr  16596  lcmftp  16605  lcmfunsnlem2  16609  divgcdcoprm0  16634  prm2orodd  16660  hashdvds  16745  oddprmdvds  16874  vdwlem12  16963  cshwshashlem1  17066  cshwsiun  17070  initoid  17968  termoid  17969  setcinv  18057  yonedainv  18247  joinfval  18337  joinfval2  18338  meetfval  18351  meetfval2  18352  latnle  18439  chnfi  18600  sgrp2nmndlem3  18896  grpid  18951  grpinvcnv  18982  grplmulf1o  18989  grpraddf1o  18990  grpsubeq0  19002  grpsubadd  19004  grplactcnv  19019  ressmulgnnd  19054  isnsg4  19142  eqg0el  19158  cycsubmel  19175  conjghm  19224  conjnmzb  19228  gacan  19280  gapm  19281  cntzrec  19311  oppgcntz  19339  fvcosymgeq  19404  odmulgeq  19532  dfod2  19539  sylow3lem3  19604  sylow3lem6  19607  lssnle  19649  lsmhash  19680  efgredlemb  19721  efgrelexlemb  19725  dprd2d2  20021  ablfac1eulem  20049  pgpfac1lem2  20052  pgpfac1lem4  20055  dvdsrval  20341  dvdsr02  20352  01eq0ring  20507  0ring01eqbi  20509  rngcinv  20614  ringcinv  20648  orngsqr  20843  rmodislmodlem  20924  lvecinv  21111  rngqiprngimf1lem  21292  rspsn  21331  prmirredlem  21452  zndvds  21529  znleval  21534  psrbagconf1o  21909  mplmonmul  22014  gsummoncoe1  22273  evl1maprhm  22344  mat1dimelbas  22436  mat1dimbas  22437  1mavmul  22513  ma1repveval  22536  mulmarep1gsum1  22538  mdetunilem9  22585  m2cpminvid2lem  22719  pmatcollpw3lem  22748  mp2pm2mplem4  22774  toponsspwpw  22887  dmtopon  22888  cmpfi  23373  ssref  23477  qtopeu  23681  hmeoimaf1o  23735  txhmeo  23768  fbasrn  23849  rnelfmlem  23917  hauspwpwf1  23952  alexsubALTlem4  24015  qustgpopn  24085  qustgphaus  24088  fmucndlem  24255  isngp3  24563  isngp4  24577  metnrmlem1a  24824  icopnfcnv  24909  iccpnfcnv  24911  ivthle  25423  ivthle2  25424  dyadmbl  25567  mbfinf  25632  i1fmulclem  25669  itg1mulc  25671  mvth  25959  dvivth  25977  lhop2  25982  r1pid2  26127  dvdsq1p  26128  reeff1o  26412  coseq1  26489  recosf1o  26499  resinf1o  26500  efopn  26622  cxpeq  26721  logreclem  26726  affineequiv  26787  affineequiv4  26790  affineequivne  26791  quad2  26803  dcubic  26810  mcubic  26811  quart  26825  atandm2  26841  rlimcnp2  26930  amgm  26954  wilthlem2  27032  mumullem2  27143  sqff1o  27145  dvdsflf1o  27150  gausslemma2dlem0i  27327  lgseisenlem2  27339  lgsquadlem2  27344  2lgslem1c  27356  2lgsoddprmlem2  27372  2lgsoddprm  27379  2sq2  27396  addsq2reu  27403  2sqreultlem  27410  2sqreunnltlem  27413  2sqreulem3  27416  ltsval2  27620  ltsintdifex  27625  ltsres  27626  nosepon  27629  noextenddif  27632  nosepssdm  27650  nogt01o  27660  nosupprefixmo  27664  noinfprefixmo  27665  nosupno  27667  noinfno  27682  lesloe  27718  eqcuts2  27778  cutbdaylt  27790  elold  27851  made0  27855  lrrecfr  27935  subadds  28062  oncutlt  28256  z12sge0  28475  renegscl  28490  tgjustf  28541  legtrid  28659  legso  28667  islmib  28855  lmicom  28856  lmiinv  28860  lmimid  28862  lmiopp  28870  colinearalglem2  28976  colinearalg  28979  ax5seglem4  29001  ax5seglem5  29002  axlowdimlem13  29023  axeuclidlem  29031  axeuclid  29032  axcontlem2  29034  axcontlem4  29036  elntg2  29054  structiedg0val  29091  uspgredgiedg  29244  uspgriedgedg  29245  usgredgsscusgredg  29528  fusgrn0degnn0  29568  umgr2v2evtxel  29591  vdiscusgrb  29599  uspgr2wlkeq  29714  wlk0prc  29721  wlklenvclwlk  29722  wlkp1lem8  29747  spthdep  29802  usgr2pthlem  29831  usgr2pth  29832  wlkiswwlksupgr2  29945  wlklnwwlkln2lem  29950  wwlksnextproplem3  29979  umgr2adedgwlk  30013  umgr2adedgspth  30016  umgr2wlkon  30018  usgrwwlks2on  30026  umgrwwlks2on  30027  elwwlks2  30037  elwspths2spth  30038  clwlkclwwlklem2a4  30067  clwlkclwwlklem2  30070  erclwwlkref  30090  clwwlkf  30117  erclwwlknref  30139  erclwwlknsym  30140  erclwwlkntr  30141  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  eupth2lem2  30289  eucrct2eupth  30315  numclwwlkqhash  30445  isgrpo  30568  hvsubaddi  31137  hire  31165  shmodsi  31460  omlsilem  31473  chcon1i  31536  chnlei  31556  pjoml3i  31657  cmbr2i  31667  chscllem2  31709  adjsym  31904  eigorthi  31908  dfadj2  31956  adjval2  31962  cnvadj  31963  dmadjrnb  31977  adjvalval  32008  cnlnadjeui  32148  cnlnssadj  32151  adjbdln  32154  pjimai  32247  pjin2i  32264  pjin3i  32265  stadd3i  32319  largei  32338  cvnbtwn3  32359  cvnbtwn4  32360  mddmd2  32380  superpos  32425  atnemeq0  32448  sumdmdii  32486  sumdmdlem  32489  addltmulALT  32517  opreu2reuALT  32546  foresf1o  32574  difeq  32588  disjrdx  32661  fcoinvbr  32675  brab2d  32678  fmptco1f1o  32706  dfimafnf  32709  curry2ima  32782  intimafv  32784  receqid  32817  elicoelioo  32851  fzo0opth  32876  wrdt2ind  33013  swrdrn3  33015  gsummptp1  33118  gsummulsubdishift1  33129  cntrval2  33232  domnprodeq0  33337  qusker  33409  dvdsrspss  33447  lsmsnorb  33451  1arithufdlem4  33607  r1pid2OLD  33669  psrmonmul  33694  esplyind  33719  algextdeglem8  33868  zarcls  34018  xrmulc1cn  34074  xrge0iifcnv  34077  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  esum2dlem  34236  issgon  34267  eulerpartgbij  34516  eulerpartlemgh  34522  ballotlemsima  34660  bnj1366  34971  bnj553  35040  bnj964  35085  fineqvnttrclse  35268  cusgredgex  35304  revwlk  35307  loop1cycl  35319  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem9  35381  prv1n  35613  ply1divalg3  35824  quad3  35852  br6  35939  elintfv  35947  dfon2lem5  35967  dfon2lem8  35970  brbigcup  36078  dfbigcup2  36079  elfix  36083  ellimits  36090  snelsingles  36102  dfiota3  36103  imageval  36110  brapply  36118  lemsuccf  36121  dfsuccf2  36123  funpartlem  36124  brfullfun  36130  dfrecs2  36132  dfrdg4  36133  altopthbg  36150  altopthc  36153  altopthd  36154  altopelaltxp  36158  brsegle  36290  outsideofrflx  36309  elicc3  36499  nn0prpw  36505  opnregcld  36512  cldregopn  36513  fneval  36534  topfneec  36537  knoppndvlem9  36780  bj-elgab  37246  bj-gabima  37247  bj-elsngl  37275  bj-snglc  37276  bj-projval  37303  bj-disj2r  37335  bj-restreg  37411  bj-0int  37413  copsex2gd  37452  copsex2b  37454  bj-inftyexpitaudisj  37519  bj-inftyexpidisj  37524  bj-bary1lem1  37625  topdifinffinlem  37663  topdifinfeq  37666  fvineqsnf1  37726  curf  37919  uncf  37920  curunc  37923  unccur  37924  poimirlem2  37943  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem27  37968  mblfinlem2  37979  mbfresfi  37987  itg2addnclem2  37993  ftc1anclem3  38016  fdc  38066  heibor1  38131  opidonOLD  38173  0rngo  38348  smprngopr  38373  isfldidl  38389  isfldidl2  38390  eqbrb  38560  eqelb  38562  ideq2  38634  relcnveq  38649  n0elqs  38653  disjressuc2  38732  dfsucmap3  38784  dfsucmap4  38786  dmsucmap  38789  preuniqval  38817  elrelscnveq  38949  qseq  39054  disjdmqscossss  39227  lcvnbtwn3  39474  lcvexchlem1  39480  lsatnem0  39491  opcon1b  39644  omllaw2N  39690  cmtbr2N  39699  leatb  39738  cvlsupr2  39789  glbconxN  39824  islln3  39956  llnexatN  39967  islpln3  39979  lplnexatN  40009  islvol3  40022  dalem-cly  40117  isline4N  40223  2llnma3r  40234  poml4N  40399  4atex2  40523  4atex2-0bOLDN  40525  cdlemefrs29bpre0  40842  cdlemftr3  41011  cdlemb3  41052  cdlemg17h  41114  cdlemg17pq  41118  cdlemg19  41130  cdlemg21  41132  tendoex  41421  dva1dim  41431  dihglb2  41788  doch11  41819  dochsordN  41820  lcfrlem9  41996  hlhillcs  42404  lcmineqlem4  42471  aks6d1c7lem2  42620  aks5lem3a  42628  aks5lem6  42631  unitscyglem2  42635  unitscyglem3  42636  addsubeq4com  42712  ef11d  42771  redivmul2d  42878  fimgmcyclem  42978  fsuppind  43023  elrfirn  43127  isnacs2  43138  isnacs3  43142  fiphp3d  43247  wopprc  43458  islnm2  43506  kercvrlsm  43511  fgraphopab  43631  tfsconcatlem  43764  tfsconcatrn  43770  tfsconcat0i  43773  tfsconcat0b  43774  tfsconcatrev  43776  oaun3lem1  43802  oadif1lem  43807  oadif1  43808  rp-fakeuninass  43943  snen1g  43951  iscard4  43960  sqrtcval  44068  frege124d  44188  frege129d  44190  frege92  44382  dffrege99  44389  clsk3nimkb  44467  clsk1indlem4  44471  clsk1indlem1  44472  ntrclsiso  44494  ntrclsk3  44497  ntrclsk13  44498  ntrneik4w  44527  extoimad  44591  int-sqdefd  44608  int-sqgeq0d  44613  radcnvrat  44741  bcc0  44767  opelopab4  44978  eqsbc2VD  45266  fzisoeu  45733  iuneqfzuz  45765  supxrleubrnmptf  45879  rexanuz2nf  45920  fsummulc1f  46001  fsumiunss  46005  fmul01lt1lem2  46015  sumnnodd  46060  fnlimfvre2  46105  limsupreuz  46165  limsupvaluz2  46166  liminfvalxr  46211  icccncfext  46315  cncfiooicc  46322  cncfioobdlem  46324  dvmptmulf  46365  dvmptfprodlem  46372  volioc  46400  itgioocnicc  46405  fourierdlem12  46547  fourierdlem20  46555  fourierdlem25  46560  fourierdlem33  46568  fourierdlem42  46577  fourierdlem52  46586  fourierdlem54  46588  fourierdlem57  46591  fourierdlem58  46592  fourierdlem59  46593  fourierdlem63  46597  fourierdlem65  46599  fourierdlem68  46602  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem80  46614  fourierdlem81  46615  rrndistlt  46718  sge0ltfirpmpt2  46854  sge0pnfmpt  46873  hoidmv1le  47022  hoidmvle  47028  vonioolem2  47109  smflimlem3  47201  chnsubseqwl  47309  cos5teq  47328  lambert0  47335  lamberte  47336  euabsneu  47476  funressnfv  47491  aiotaval  47543  reuf1odnf  47555  reuf1od  47556  afvpcfv0  47594  dfafn5a  47608  afvelrnb  47611  afvelrnb0  47612  dfaimafn2  47614  dfatsnafv2  47700  dfatdmfcoafv2  47702  f1oresf1o2  47739  ceilbi  47785  minusmodnep2tmod  47807  0nelsetpreimafv  47850  fargshiftfo  47902  sprsymrelf1  47956  reupr  47982  nprmmul1  47987  fmtnorec2lem  48005  fmtnoprmfac1  48028  fmtnoprmfac2  48030  sfprmdvdsmersenne  48066  lighneallem2  48069  dfeven2  48125  dfodd3  48126  odd2np1ALTV  48150  even3prm2  48195  fppr2odd  48207  nnsum3primesgbe  48268  nnsum3primesle9  48270  clnbgrsym  48314  dfvopnbgr2  48329  isuspgrim0  48370  isuspgrimlem  48371  dfgric2  48391  grtriprop  48417  uspgrlimlem3  48466  gpgvtxedg1  48540  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  0nodd  48646  2nodd  48648  lmod0rng  48705  rngcinvALTV  48752  ringcinvALTV  48786  lcoel0  48904  lindslinindimp2lem4  48937  ldepspr  48949  lincresunit3  48957  nn0sumshdiglemB  49096  nn0sumshdiglem1  49097  rrx2pnedifcoorneorr  49193  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2linest  49218  rrx2linest2  49220  rrxsphere  49224  line2ylem  49227  line2x  49230  itscnhlc0xyqsol  49241  itschlc0xyqsol1  49242  itsclinecirc0b  49250  2itscp  49257  inlinecirc02plem  49262  brab2dd  49303  uptr2  49696