Theorem eqcom 2744

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 2743	. 2 ⊢ (𝐴 = 𝐵 → 𝐵 = 𝐴)
3		id 22	. . 3 ⊢ (𝐵 = 𝐴 → 𝐵 = 𝐴)
4	3	eqcomd 2743	. 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 2709

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

This theorem is referenced by:  eqcoms  2745  eqcomi  2746  neqcomd  2747  eqeq2d  2748  eqabcbw  2811  eqabcb  2877  necom  2986  nesym  2989  gencbvex  3488  clel5  3608  eqsbc2  3793  dfss  3909  sspsstri  4046  ssdifim  4214  disj4  4400  reuprg0  4647  preq1b  4790  invdisj  5072  disjprg  5082  dtruALT  5326  reusv3  5343  opthg2  5428  copsex2g  5442  copsex4g  5444  opcom  5450  opeqsng  5452  opeqpr  5454  snopeqop  5455  propeqop  5456  opthwiener  5463  vopelopabsb  5478  opthprc  5689  elxp3  5691  relop  5800  dmopab3  5869  rnopab3  5906  rncoeq  5932  restidsing  6013  somin1  6091  xpcan  6135  xpcan2  6136  dfrel4v  6149  dmsnn0  6166  reu3op  6251  reuop  6252  opreu2reurex  6253  ordtri2  6353  ordtri2or3  6420  suc11  6427  on0eqel  6443  snsn0non  6444  iota1  6472  iotan0  6483  sniota  6484  mptfnf  6628  fresaunres1  6708  dffn5  6893  fvelrnb  6895  dfimafn2  6898  funimass4  6899  feqmptdf  6905  fnsnfv  6914  dmfco  6931  funcnvmpt  6944  fndmdif  6989  fneqeql  6993  rexrn  7034  ralrn  7035  elrnrexdmb  7037  dffo4  7050  fssrescdmd  7074  funopsn  7096  ftpg  7104  fprb  7143  ralima  7186  reximaOLD  7188  ralimaOLD  7189  fvclss  7190  dff13  7203  f1eqcocnv  7250  fnssintima  7311  imaeqsexvOLD  7312  riotaeqimp  7344  eusvobj2  7353  f1ocnvfv3  7356  oprabidw  7392  oprabid  7393  oprabv  7421  eloprabga  7470  ovelimab  7539  onmindif2  7755  br1steqg  7958  br2ndeqg  7959  dfoprab3  8001  opiota  8006  f1o2ndf1  8066  soseq  8103  brtpos2  8176  tpossym  8202  mpocurryd  8213  rdglim2  8365  tz7.48lem  8374  oaf1o  8492  omopthi  8591  erth2  8693  brecop  8751  erovlem  8754  ecopovsym  8760  eceqoveq  8763  xpcomco  8999  omxpenlem  9010  mapen  9073  nneneq  9134  unxpdomlem3  9162  unfilem1  9209  mapfien  9315  supgtoreq  9378  wemapsolem  9459  suc11reg  9534  inf3lem2  9544  inf3lem6  9548  ttrcltr  9631  djulf1o  9830  djurf1o  9831  infenaleph  10007  isinfcard  10008  dfac5  10045  cfeq0  10172  cfsuc  10173  ssfin4  10226  fin23lem25  10240  fin23lem22  10243  fin23lem40  10267  fin1a2lem5  10320  axcclem  10373  brdom7disj  10447  brdom6disj  10448  inar1  10692  psslinpr  10948  ltexprlem4  10956  ltsrpr  10994  mulgt0sr  11022  elreal  11048  ltresr  11057  leloe  11226  eqlei2  11251  addsubeq4  11402  subcan2  11413  negcon1  11440  negcon2  11441  addid0  11563  addeq0  11567  divmul2  11807  conjmul  11866  rereccl  11867  creur  12147  creui  12148  ind1a  12164  nndiv  12217  nn0sub  12481  elnn0z  12531  elznn0  12533  xrleloe  13089  ngtmnft  13112  icoshftf1o  13421  iccf1o  13443  fzen  13489  fzneuz  13556  injresinj  13740  fleqceilz  13807  mod0  13829  modmuladdnn0  13871  modirr  13898  addmodlteq  13902  nn0ennn  13935  hashrabsn01  14329  hashsdom  14337  hashgt12el2  14379  hashbclem  14408  hashfacen  14410  hashf1lem1  14411  hashtpg  14441  tpf1o  14457  fi1uzind  14463  ccatw2s1p1  14593  wrd2ind  14679  cshw1  14778  cshwsexa  14780  scshwfzeqfzo  14782  s2f1o  14872  wwlktovfo  14914  dmtrclfv  14974  cjreb  15079  leabs  15255  reusq0  15421  incexc2  15797  rpnnen2lem12  16186  dvdsval2  16218  dvdsabseq  16276  dvdsflip  16280  odd2np1  16304  oddm1even  16306  sqoddm1div8z  16317  m1exp1  16339  divalglem4  16359  divalglem8  16363  divalgb  16367  modremain  16371  zeqzmulgcd  16473  dfgcd2  16509  lcmfpr  16590  lcmftp  16599  lcmfunsnlem2  16603  divgcdcoprm0  16628  prm2orodd  16654  hashdvds  16739  oddprmdvds  16868  vdwlem12  16957  cshwshashlem1  17060  cshwsiun  17064  initoid  17962  termoid  17963  setcinv  18051  yonedainv  18241  joinfval  18331  joinfval2  18332  meetfval  18345  meetfval2  18346  latnle  18433  chnfi  18594  sgrp2nmndlem3  18890  grpid  18945  grpinvcnv  18976  grplmulf1o  18983  grpraddf1o  18984  grpsubeq0  18996  grpsubadd  18998  grplactcnv  19013  ressmulgnnd  19048  isnsg4  19136  eqg0el  19152  cycsubmel  19169  conjghm  19218  conjnmzb  19222  gacan  19274  gapm  19275  cntzrec  19305  oppgcntz  19333  fvcosymgeq  19398  odmulgeq  19526  dfod2  19533  sylow3lem3  19598  sylow3lem6  19601  lssnle  19643  lsmhash  19674  efgredlemb  19715  efgrelexlemb  19719  dprd2d2  20015  ablfac1eulem  20043  pgpfac1lem2  20046  pgpfac1lem4  20049  dvdsrval  20335  dvdsr02  20346  01eq0ring  20501  0ring01eqbi  20503  rngcinv  20608  ringcinv  20642  orngsqr  20837  rmodislmodlem  20918  lvecinv  21106  rngqiprngimf1lem  21287  rspsn  21326  dfcnfldOLD  21363  prmirredlem  21465  zndvds  21542  znleval  21547  psrbagconf1o  21922  mplmonmul  22027  gsummoncoe1  22286  evl1maprhm  22357  mat1dimelbas  22449  mat1dimbas  22450  1mavmul  22526  ma1repveval  22549  mulmarep1gsum1  22551  mdetunilem9  22598  m2cpminvid2lem  22732  pmatcollpw3lem  22761  mp2pm2mplem4  22787  toponsspwpw  22900  dmtopon  22901  cmpfi  23386  ssref  23490  qtopeu  23694  hmeoimaf1o  23748  txhmeo  23781  fbasrn  23862  rnelfmlem  23930  hauspwpwf1  23965  alexsubALTlem4  24028  qustgpopn  24098  qustgphaus  24101  fmucndlem  24268  isngp3  24576  isngp4  24590  metnrmlem1a  24837  icopnfcnv  24922  iccpnfcnv  24924  ivthle  25436  ivthle2  25437  dyadmbl  25580  mbfinf  25645  i1fmulclem  25682  itg1mulc  25684  mvth  25972  dvivth  25990  lhop2  25995  r1pid2  26140  dvdsq1p  26141  reeff1o  26428  coseq1  26505  recosf1o  26515  resinf1o  26516  efopn  26638  cxpeq  26737  logreclem  26742  affineequiv  26803  affineequiv4  26806  affineequivne  26807  quad2  26819  dcubic  26826  mcubic  26827  quart  26841  atandm2  26857  rlimcnp2  26946  amgm  26971  wilthlem2  27049  mumullem2  27160  sqff1o  27162  dvdsflf1o  27167  gausslemma2dlem0i  27344  lgseisenlem2  27356  lgsquadlem2  27361  2lgslem1c  27373  2lgsoddprmlem2  27389  2lgsoddprm  27396  2sq2  27413  addsq2reu  27420  2sqreultlem  27427  2sqreunnltlem  27430  2sqreulem3  27433  ltsval2  27637  ltsintdifex  27642  ltsres  27643  nosepon  27646  noextenddif  27649  nosepssdm  27667  nogt01o  27677  nosupprefixmo  27681  noinfprefixmo  27682  nosupno  27684  noinfno  27699  lesloe  27735  eqcuts2  27795  cutbdaylt  27807  elold  27868  made0  27872  lrrecfr  27952  subadds  28079  oncutlt  28273  z12sge0  28492  renegscl  28507  tgjustf  28558  legtrid  28676  legso  28684  islmib  28872  lmicom  28873  lmiinv  28877  lmimid  28879  lmiopp  28887  colinearalglem2  28993  colinearalg  28996  ax5seglem4  29018  ax5seglem5  29019  axlowdimlem13  29040  axeuclidlem  29048  axeuclid  29049  axcontlem2  29051  axcontlem4  29053  elntg2  29071  structiedg0val  29108  uspgredgiedg  29261  uspgriedgedg  29262  usgredgsscusgredg  29546  fusgrn0degnn0  29586  umgr2v2evtxel  29609  vdiscusgrb  29617  uspgr2wlkeq  29732  wlk0prc  29739  wlklenvclwlk  29740  wlkp1lem8  29765  spthdep  29820  usgr2pthlem  29849  usgr2pth  29850  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  wwlksnextproplem3  29997  umgr2adedgwlk  30031  umgr2adedgspth  30034  umgr2wlkon  30036  usgrwwlks2on  30044  umgrwwlks2on  30045  elwwlks2  30055  elwspths2spth  30056  clwlkclwwlklem2a4  30085  clwlkclwwlklem2  30088  erclwwlkref  30108  clwwlkf  30135  erclwwlknref  30157  erclwwlknsym  30158  erclwwlkntr  30159  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  eupth2lem2  30307  eucrct2eupth  30333  numclwwlkqhash  30463  isgrpo  30586  hvsubaddi  31155  hire  31183  shmodsi  31478  omlsilem  31491  chcon1i  31554  chnlei  31574  pjoml3i  31675  cmbr2i  31685  chscllem2  31727  adjsym  31922  eigorthi  31926  dfadj2  31974  adjval2  31980  cnvadj  31981  dmadjrnb  31995  adjvalval  32026  cnlnadjeui  32166  cnlnssadj  32169  adjbdln  32172  pjimai  32265  pjin2i  32282  pjin3i  32283  stadd3i  32337  largei  32356  cvnbtwn3  32377  cvnbtwn4  32378  mddmd2  32398  superpos  32443  atnemeq0  32466  sumdmdii  32504  sumdmdlem  32507  addltmulALT  32535  opreu2reuALT  32564  foresf1o  32592  difeq  32606  disjrdx  32679  fcoinvbr  32693  brab2d  32696  fmptco1f1o  32724  dfimafnf  32727  curry2ima  32800  intimafv  32802  receqid  32835  elicoelioo  32869  fzo0opth  32894  wrdt2ind  33031  swrdrn3  33033  gsummptp1  33136  gsummulsubdishift1  33147  cntrval2  33250  domnprodeq0  33355  qusker  33427  dvdsrspss  33465  lsmsnorb  33469  1arithufdlem4  33625  r1pid2OLD  33687  psrmonmul  33712  esplyind  33737  algextdeglem8  33887  zarcls  34037  xrmulc1cn  34093  xrge0iifcnv  34096  esumfsup  34233  esumpcvgval  34241  esumcvg  34249  esum2dlem  34255  issgon  34286  eulerpartgbij  34535  eulerpartlemgh  34541  ballotlemsima  34679  bnj1366  34990  bnj553  35059  bnj964  35104  fineqvnttrclse  35287  cusgredgex  35323  revwlk  35326  loop1cycl  35338  subfacp1lem3  35383  subfacp1lem5  35385  erdszelem9  35400  prv1n  35632  ply1divalg3  35843  quad3  35871  br6  35958  elintfv  35966  dfon2lem5  35986  dfon2lem8  35989  brbigcup  36097  dfbigcup2  36098  elfix  36102  ellimits  36109  snelsingles  36121  dfiota3  36122  imageval  36129  brapply  36137  lemsuccf  36140  dfsuccf2  36142  funpartlem  36143  brfullfun  36149  dfrecs2  36151  dfrdg4  36152  altopthbg  36169  altopthc  36172  altopthd  36173  altopelaltxp  36177  brsegle  36309  outsideofrflx  36328  elicc3  36518  nn0prpw  36524  opnregcld  36531  cldregopn  36532  fneval  36553  topfneec  36556  knoppndvlem9  36799  bj-elgab  37265  bj-gabima  37266  bj-elsngl  37294  bj-snglc  37295  bj-projval  37322  bj-disj2r  37354  bj-restreg  37430  bj-0int  37432  copsex2gd  37471  copsex2b  37473  bj-inftyexpitaudisj  37538  bj-inftyexpidisj  37543  bj-bary1lem1  37644  topdifinffinlem  37680  topdifinfeq  37683  fvineqsnf1  37743  curf  37936  uncf  37937  curunc  37940  unccur  37941  poimirlem2  37960  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem27  37985  mblfinlem2  37996  mbfresfi  38004  itg2addnclem2  38010  ftc1anclem3  38033  fdc  38083  heibor1  38148  opidonOLD  38190  0rngo  38365  smprngopr  38390  isfldidl  38406  isfldidl2  38407  eqbrb  38577  eqelb  38579  ideq2  38651  relcnveq  38666  n0elqs  38670  disjressuc2  38749  dfsucmap3  38801  dfsucmap4  38803  dmsucmap  38806  preuniqval  38834  elrelscnveq  38966  qseq  39071  disjdmqscossss  39244  lcvnbtwn3  39491  lcvexchlem1  39497  lsatnem0  39508  opcon1b  39661  omllaw2N  39707  cmtbr2N  39716  leatb  39755  cvlsupr2  39806  glbconxN  39841  islln3  39973  llnexatN  39984  islpln3  39996  lplnexatN  40026  islvol3  40039  dalem-cly  40134  isline4N  40240  2llnma3r  40251  poml4N  40416  4atex2  40540  4atex2-0bOLDN  40542  cdlemefrs29bpre0  40859  cdlemftr3  41028  cdlemb3  41069  cdlemg17h  41131  cdlemg17pq  41135  cdlemg19  41147  cdlemg21  41149  tendoex  41438  dva1dim  41448  dihglb2  41805  doch11  41836  dochsordN  41837  lcfrlem9  42013  hlhillcs  42421  lcmineqlem4  42488  aks6d1c7lem2  42637  aks5lem3a  42645  aks5lem6  42648  unitscyglem2  42652  unitscyglem3  42653  addsubeq4com  42729  ef11d  42788  redivmul2d  42895  fimgmcyclem  42995  fsuppind  43040  elrfirn  43144  isnacs2  43155  isnacs3  43159  fiphp3d  43268  wopprc  43479  islnm2  43527  kercvrlsm  43532  fgraphopab  43652  tfsconcatlem  43785  tfsconcatrn  43791  tfsconcat0i  43794  tfsconcat0b  43795  tfsconcatrev  43797  oaun3lem1  43823  oadif1lem  43828  oadif1  43829  rp-fakeuninass  43964  snen1g  43972  iscard4  43981  sqrtcval  44089  frege124d  44209  frege129d  44211  frege92  44403  dffrege99  44410  clsk3nimkb  44488  clsk1indlem4  44492  clsk1indlem1  44493  ntrclsiso  44515  ntrclsk3  44518  ntrclsk13  44519  ntrneik4w  44548  extoimad  44612  int-sqdefd  44629  int-sqgeq0d  44634  radcnvrat  44762  bcc0  44788  opelopab4  44999  eqsbc2VD  45287  fzisoeu  45754  iuneqfzuz  45786  supxrleubrnmptf  45900  rexanuz2nf  45941  fsummulc1f  46022  fsumiunss  46026  fmul01lt1lem2  46036  sumnnodd  46081  fnlimfvre2  46126  limsupreuz  46186  limsupvaluz2  46187  liminfvalxr  46232  icccncfext  46336  cncfiooicc  46343  cncfioobdlem  46345  dvmptmulf  46386  dvmptfprodlem  46393  volioc  46421  itgioocnicc  46426  fourierdlem12  46568  fourierdlem20  46576  fourierdlem25  46581  fourierdlem33  46589  fourierdlem42  46598  fourierdlem52  46607  fourierdlem54  46609  fourierdlem57  46612  fourierdlem58  46613  fourierdlem59  46614  fourierdlem63  46618  fourierdlem65  46620  fourierdlem68  46623  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem80  46635  fourierdlem81  46636  rrndistlt  46739  sge0ltfirpmpt2  46875  sge0pnfmpt  46894  hoidmv1le  47043  hoidmvle  47049  vonioolem2  47130  smflimlem3  47222  chnsubseqwl  47328  lambert0  47350  lamberte  47351  euabsneu  47491  funressnfv  47506  aiotaval  47558  reuf1odnf  47570  reuf1od  47571  afvpcfv0  47609  dfafn5a  47623  afvelrnb  47626  afvelrnb0  47627  dfaimafn2  47629  dfatsnafv2  47715  dfatdmfcoafv2  47717  f1oresf1o2  47754  ceilbi  47800  minusmodnep2tmod  47822  0nelsetpreimafv  47865  fargshiftfo  47917  sprsymrelf1  47971  reupr  47997  nprmmul1  48002  fmtnorec2lem  48020  fmtnoprmfac1  48043  fmtnoprmfac2  48045  sfprmdvdsmersenne  48081  lighneallem2  48084  dfeven2  48140  dfodd3  48141  odd2np1ALTV  48165  even3prm2  48210  fppr2odd  48222  nnsum3primesgbe  48283  nnsum3primesle9  48285  clnbgrsym  48329  dfvopnbgr2  48344  isuspgrim0  48385  isuspgrimlem  48386  dfgric2  48406  grtriprop  48432  uspgrlimlem3  48481  gpgvtxedg1  48555  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  0nodd  48661  2nodd  48663  lmod0rng  48720  rngcinvALTV  48767  ringcinvALTV  48801  lcoel0  48919  lindslinindimp2lem4  48952  ldepspr  48964  lincresunit3  48972  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  rrx2pnedifcoorneorr  49208  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  rrx2linest  49233  rrx2linest2  49235  rrxsphere  49239  line2ylem  49242  line2x  49245  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  itsclinecirc0b  49265  2itscp  49272  inlinecirc02plem  49277  brab2dd  49318  uptr2  49711