Theorem eqcom 2736

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqcoms  2737  eqcomi  2738  neqcomd  2739  eqeq2d  2740  eqabcb  2869  necom  2978  nesym  2981  gencbvex  3507  clel5  3631  eqsbc2  3817  dfss  3933  sspsstri  4068  ssnelpss  4077  ssdifim  4236  disj  4413  disj4  4422  reuprg0  4666  preq1b  4810  invdisj  5093  disjprg  5103  dtruALT  5343  reusv3  5360  opthg2  5439  copsex2g  5453  copsex4g  5455  opcom  5461  opeqsng  5463  opeqpr  5465  snopeqop  5466  propeqop  5467  opthwiener  5474  vopelopabsb  5489  opthprc  5702  elxp3  5704  relop  5814  dmopab3  5883  rnopab3  5920  rncoeq  5943  restidsing  6024  somin1  6106  xpcan  6149  xpcan2  6150  dfrel4v  6163  dmsnn0  6180  reu3op  6265  reuop  6266  opreu2reurex  6267  ordtri2  6367  ordtri2or3  6434  suc11  6441  on0eqel  6458  snsn0non  6459  iota1  6488  iotan0  6501  sniota  6502  mptfnf  6653  fresaunres1  6733  dffn5  6919  fvelrnb  6921  dfimafn2  6924  funimass4  6925  feqmptdf  6931  fnsnfv  6940  dmfco  6957  fndmdif  7014  fneqeql  7018  rexrn  7059  ralrn  7060  elrnrexdmb  7062  dffo4  7075  fssrescdmd  7098  funopsn  7120  ftpg  7128  fprb  7168  ralima  7211  reximaOLD  7213  ralimaOLD  7214  fvclss  7215  dff13  7229  f1eqcocnv  7276  fnssintima  7337  imaeqsexvOLD  7338  riotaeqimp  7370  eusvobj2  7379  f1ocnvfv3  7382  oprabidw  7418  oprabid  7419  oprabv  7449  eloprabga  7498  ovelimab  7567  onmindif2  7783  br1steqg  7990  br2ndeqg  7991  dfoprab3  8033  opiota  8038  f1o2ndf1  8101  soseq  8138  brtpos2  8211  tpossym  8237  mpocurryd  8248  rdglim2  8400  tz7.48lem  8409  oaf1o  8527  omopthi  8625  erth2  8726  brecop  8783  erovlem  8786  ecopovsym  8792  eceqoveq  8795  xpcomco  9031  omxpenlem  9042  mapen  9105  nneneq  9170  unxpdomlem3  9199  unfilem1  9254  mapfien  9359  supgtoreq  9422  wemapsolem  9503  suc11reg  9572  inf3lem2  9582  inf3lem6  9586  ttrcltr  9669  djulf1o  9865  djurf1o  9866  infenaleph  10044  isinfcard  10045  dfac5  10082  cfeq0  10209  cfsuc  10210  ssfin4  10263  fin23lem25  10277  fin23lem22  10280  fin23lem40  10304  fin1a2lem5  10357  axcclem  10410  brdom7disj  10484  brdom6disj  10485  inar1  10728  psslinpr  10984  ltexprlem4  10992  ltsrpr  11030  mulgt0sr  11058  elreal  11084  ltresr  11093  leloe  11260  eqlei2  11285  addsubeq4  11436  subcan2  11447  negcon1  11474  negcon2  11475  addid0  11597  addeq0  11601  divmul2  11841  conjmul  11899  rereccl  11900  creur  12180  creui  12181  nndiv  12232  nn0sub  12492  elnn0z  12542  elznn0  12544  xrleloe  13104  ngtmnft  13126  icoshftf1o  13435  iccf1o  13457  fzen  13502  fzneuz  13569  injresinj  13749  fleqceilz  13816  mod0  13838  modmuladdnn0  13880  modirr  13907  addmodlteq  13911  nn0ennn  13944  hashrabsn01  14338  hashsdom  14346  hashgt12el2  14388  hashbclem  14417  hashfacen  14419  hashf1lem1  14420  hashtpg  14450  tpf1o  14466  fi1uzind  14472  ccatw2s1p1  14601  wrd2ind  14688  cshw1  14787  cshwsexa  14789  scshwfzeqfzo  14792  s2f1o  14882  wwlktovfo  14924  dmtrclfv  14984  cjreb  15089  leabs  15265  reusq0  15431  incexc2  15804  rpnnen2lem12  16193  dvdsval2  16225  dvdsabseq  16283  dvdsflip  16287  odd2np1  16311  oddm1even  16313  sqoddm1div8z  16324  m1exp1  16346  divalglem4  16366  divalglem8  16370  divalgb  16374  modremain  16378  zeqzmulgcd  16480  dfgcd2  16516  lcmfpr  16597  lcmftp  16606  lcmfunsnlem2  16610  divgcdcoprm0  16635  prm2orodd  16661  hashdvds  16745  oddprmdvds  16874  vdwlem12  16963  cshwshashlem1  17066  cshwsiun  17070  initoid  17963  termoid  17964  setcinv  18052  yonedainv  18242  joinfval  18332  joinfval2  18333  meetfval  18346  meetfval2  18347  latnle  18432  sgrp2nmndlem3  18852  grpid  18907  grpinvcnv  18938  grplmulf1o  18945  grpraddf1o  18946  grpsubeq0  18958  grpsubadd  18960  grplactcnv  18975  ressmulgnnd  19010  isnsg4  19099  eqg0el  19115  cycsubmel  19132  conjghm  19181  conjnmzb  19185  gacan  19237  gapm  19238  cntzrec  19268  oppgcntz  19296  fvcosymgeq  19359  odmulgeq  19487  dfod2  19494  sylow3lem3  19559  sylow3lem6  19562  lssnle  19604  lsmhash  19635  efgredlemb  19676  efgrelexlemb  19680  dprd2d2  19976  ablfac1eulem  20004  pgpfac1lem2  20007  pgpfac1lem4  20010  dvdsrval  20270  dvdsr02  20281  01eq0ring  20439  0ring01eqbi  20441  rngcinv  20546  ringcinv  20580  rmodislmodlem  20835  lvecinv  21023  rngqiprngimf1lem  21204  rspsn  21243  dfcnfldOLD  21280  prmirredlem  21382  zndvds  21459  znleval  21464  psrbagconf1o  21838  mplmonmul  21943  gsummoncoe1  22195  evl1maprhm  22266  mat1dimelbas  22358  mat1dimbas  22359  1mavmul  22435  ma1repveval  22458  mulmarep1gsum1  22460  mdetunilem9  22507  m2cpminvid2lem  22641  pmatcollpw3lem  22670  mp2pm2mplem4  22696  toponsspwpw  22809  dmtopon  22810  cmpfi  23295  ssref  23399  qtopeu  23603  hmeoimaf1o  23657  txhmeo  23690  fbasrn  23771  rnelfmlem  23839  hauspwpwf1  23874  alexsubALTlem4  23937  qustgpopn  24007  qustgphaus  24010  fmucndlem  24178  isngp3  24486  isngp4  24500  metnrmlem1a  24747  icopnfcnv  24840  iccpnfcnv  24842  ivthle  25357  ivthle2  25358  dyadmbl  25501  mbfinf  25566  i1fmulclem  25603  itg1mulc  25605  mvth  25897  dvivth  25915  lhop2  25920  r1pid2  26067  dvdsq1p  26068  reeff1o  26357  coseq1  26434  recosf1o  26444  resinf1o  26445  efopn  26567  cxpeq  26667  logreclem  26672  affineequiv  26733  affineequiv4  26736  affineequivne  26737  quad2  26749  dcubic  26756  mcubic  26757  quart  26771  atandm2  26787  rlimcnp2  26876  amgm  26901  wilthlem2  26979  mumullem2  27090  sqff1o  27092  dvdsflf1o  27097  gausslemma2dlem0i  27275  lgseisenlem2  27287  lgsquadlem2  27292  2lgslem1c  27304  2lgsoddprmlem2  27320  2lgsoddprm  27327  2sq2  27344  addsq2reu  27351  2sqreultlem  27358  2sqreunnltlem  27361  2sqreulem3  27364  sltval2  27568  sltintdifex  27573  sltres  27574  nosepon  27577  noextenddif  27580  nosepssdm  27598  nogt01o  27608  nosupprefixmo  27612  noinfprefixmo  27613  nosupno  27615  noinfno  27630  sleloe  27666  eqscut2  27718  scutbdaylt  27730  elold  27781  made0  27785  lrrecfr  27850  subadds  27974  onscutlt  28165  zs12ge0  28342  renegscl  28349  tgjustf  28400  legtrid  28518  legso  28526  islmib  28714  lmicom  28715  lmiinv  28719  lmimid  28721  lmiopp  28729  colinearalglem2  28834  colinearalg  28837  ax5seglem4  28859  ax5seglem5  28860  axlowdimlem13  28881  axeuclidlem  28889  axeuclid  28890  axcontlem2  28892  axcontlem4  28894  elntg2  28912  structiedg0val  28949  uspgredgiedg  29102  uspgriedgedg  29103  usgredgsscusgredg  29387  fusgrn0degnn0  29427  umgr2v2evtxel  29450  vdiscusgrb  29458  uspgr2wlkeq  29574  wlk0prc  29582  wlklenvclwlk  29583  wlkp1lem8  29608  spthdep  29664  usgr2pthlem  29693  usgr2pth  29694  wlkiswwlksupgr2  29807  wlklnwwlkln2lem  29812  wwlksnextproplem3  29841  umgr2adedgwlk  29875  umgr2adedgspth  29878  umgr2wlkon  29880  umgrwwlks2on  29887  elwwlks2  29896  elwspths2spth  29897  clwlkclwwlklem2a4  29926  clwlkclwwlklem2  29929  erclwwlkref  29949  clwwlkf  29976  erclwwlknref  29998  erclwwlknsym  29999  erclwwlkntr  30000  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  eupth2lem2  30148  eucrct2eupth  30174  numclwwlkqhash  30304  isgrpo  30426  hvsubaddi  30995  hire  31023  shmodsi  31318  omlsilem  31331  chcon1i  31394  chnlei  31414  pjoml3i  31515  cmbr2i  31525  chscllem2  31567  adjsym  31762  eigorthi  31766  dfadj2  31814  adjval2  31820  cnvadj  31821  dmadjrnb  31835  adjvalval  31866  cnlnadjeui  32006  cnlnssadj  32009  adjbdln  32012  pjimai  32105  pjin2i  32122  pjin3i  32123  stadd3i  32177  largei  32196  cvnbtwn3  32217  cvnbtwn4  32218  mddmd2  32238  superpos  32283  atnemeq0  32306  sumdmdii  32344  sumdmdlem  32347  addltmulALT  32375  opreu2reuALT  32406  foresf1o  32433  difeq  32447  disjrdx  32520  fcoinvbr  32534  brab2d  32535  fmptco1f1o  32557  dfimafnf  32560  funcnvmpt  32591  curry2ima  32632  intimafv  32634  receqid  32668  elicoelioo  32701  fzo0opth  32728  ind1a  32782  wrdt2ind  32875  swrdrn3  32877  cntrval2  33128  orngsqr  33282  qusker  33320  dvdsrspss  33358  lsmsnorb  33362  1arithufdlem4  33518  r1pid2OLD  33574  algextdeglem8  33714  zarcls  33864  xrmulc1cn  33920  xrge0iifcnv  33923  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  esum2dlem  34082  issgon  34113  eulerpartgbij  34363  eulerpartlemgh  34369  ballotlemsima  34507  bnj1366  34819  bnj553  34888  bnj964  34933  cusgredgex  35109  revwlk  35112  loop1cycl  35124  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem9  35186  prv1n  35418  ply1divalg3  35629  quad3  35657  br6  35744  elintfv  35752  dfon2lem5  35775  dfon2lem8  35778  brbigcup  35886  dfbigcup2  35887  elfix  35891  ellimits  35898  snelsingles  35910  dfiota3  35911  imageval  35918  brapply  35926  brsuccf  35929  funpartlem  35930  brfullfun  35936  dfrecs2  35938  dfrdg4  35939  altopthbg  35956  altopthc  35959  altopthd  35960  altopelaltxp  35964  brsegle  36096  outsideofrflx  36115  elicc3  36305  nn0prpw  36311  opnregcld  36318  cldregopn  36319  fneval  36340  topfneec  36343  knoppndvlem9  36508  bj-elgab  36927  bj-gabima  36928  bj-elsngl  36956  bj-snglc  36957  bj-projval  36984  bj-disj2r  37016  bj-restreg  37087  bj-0int  37089  copsex2b  37128  bj-inftyexpitaudisj  37193  bj-inftyexpidisj  37198  bj-bary1lem1  37299  topdifinffinlem  37335  topdifinfeq  37338  fvineqsnf1  37398  curf  37592  uncf  37593  curunc  37596  unccur  37597  poimirlem2  37616  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem27  37641  mblfinlem2  37652  mbfresfi  37660  itg2addnclem2  37666  ftc1anclem3  37689  fdc  37739  heibor1  37804  opidonOLD  37846  0rngo  38021  smprngopr  38046  isfldidl  38062  isfldidl2  38063  eqbrb  38221  eqelb  38223  ideq2  38295  relcnveq  38310  n0elqs  38314  disjressuc2  38374  elrelscnveq  38483  qseq  38640  disjdmqscossss  38795  lcvnbtwn3  39021  lcvexchlem1  39027  lsatnem0  39038  opcon1b  39191  omllaw2N  39237  cmtbr2N  39246  leatb  39285  cvlsupr2  39336  glbconxN  39372  islln3  39504  llnexatN  39515  islpln3  39527  lplnexatN  39557  islvol3  39570  dalem-cly  39665  isline4N  39771  2llnma3r  39782  poml4N  39947  4atex2  40071  4atex2-0bOLDN  40073  cdlemefrs29bpre0  40390  cdlemftr3  40559  cdlemb3  40600  cdlemg17h  40662  cdlemg17pq  40666  cdlemg19  40678  cdlemg21  40680  tendoex  40969  dva1dim  40979  dihglb2  41336  doch11  41367  dochsordN  41368  lcfrlem9  41544  hlhillcs  41952  lcmineqlem4  42020  aks6d1c7lem2  42169  aks5lem3a  42177  aks5lem6  42180  unitscyglem2  42184  unitscyglem3  42185  addsubeq4com  42268  ef11d  42327  fimgmcyclem  42521  fsuppind  42578  elrfirn  42683  isnacs2  42694  isnacs3  42698  fiphp3d  42807  wopprc  43019  islnm2  43067  kercvrlsm  43072  fgraphopab  43192  tfsconcatlem  43325  tfsconcatrn  43331  tfsconcat0i  43334  tfsconcat0b  43335  tfsconcatrev  43337  oaun3lem1  43363  oadif1lem  43368  oadif1  43369  rp-fakeuninass  43505  snen1g  43513  iscard4  43522  sqrtcval  43630  frege124d  43750  frege129d  43752  frege92  43944  dffrege99  43951  clsk3nimkb  44029  clsk1indlem4  44033  clsk1indlem1  44034  ntrclsiso  44056  ntrclsk3  44059  ntrclsk13  44060  ntrneik4w  44089  extoimad  44153  int-sqdefd  44170  int-sqgeq0d  44175  radcnvrat  44303  bcc0  44329  opelopab4  44541  eqsbc2VD  44829  fzisoeu  45298  iuneqfzuz  45331  supxrleubrnmptf  45447  rexanuz2nf  45488  fsummulc1f  45569  fsumiunss  45573  fmul01lt1lem2  45583  sumnnodd  45628  fnlimfvre2  45675  limsupreuz  45735  limsupvaluz2  45736  liminfvalxr  45781  icccncfext  45885  cncfiooicc  45892  cncfioobdlem  45894  dvmptmulf  45935  dvmptfprodlem  45942  volioc  45970  itgioocnicc  45975  fourierdlem12  46117  fourierdlem20  46125  fourierdlem25  46130  fourierdlem33  46138  fourierdlem42  46147  fourierdlem52  46156  fourierdlem54  46158  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem63  46167  fourierdlem65  46169  fourierdlem68  46172  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem80  46184  fourierdlem81  46185  rrndistlt  46288  sge0ltfirpmpt2  46424  sge0pnfmpt  46443  hoidmv1le  46592  hoidmvle  46598  vonioolem2  46679  smflimlem3  46771  lambert0  46888  lamberte  46889  euabsneu  47029  funressnfv  47044  aiotaval  47096  reuf1odnf  47108  reuf1od  47109  afvpcfv0  47147  dfafn5a  47161  afvelrnb  47164  afvelrnb0  47165  dfaimafn2  47167  dfatsnafv2  47253  dfatdmfcoafv2  47255  f1oresf1o2  47292  ceilbi  47334  minusmodnep2tmod  47354  0nelsetpreimafv  47391  fargshiftfo  47443  sprsymrelf1  47497  reupr  47523  fmtnorec2lem  47543  fmtnoprmfac1  47566  fmtnoprmfac2  47568  sfprmdvdsmersenne  47604  lighneallem2  47607  dfeven2  47650  dfodd3  47651  odd2np1ALTV  47675  even3prm2  47720  fppr2odd  47732  nnsum3primesgbe  47793  nnsum3primesle9  47795  clnbgrsym  47838  dfvopnbgr2  47853  isuspgrim0  47894  isuspgrimlem  47895  dfgric2  47915  grtriprop  47940  uspgrlimlem3  47989  gpgvtxedg1  48055  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  0nodd  48158  2nodd  48160  lmod0rng  48217  rngcinvALTV  48264  ringcinvALTV  48298  lcoel0  48417  lindslinindimp2lem4  48450  ldepspr  48462  lincresunit3  48470  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  rrx2pnedifcoorneorr  48706  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2linest  48731  rrx2linest2  48733  rrxsphere  48737  line2ylem  48740  line2x  48743  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itsclinecirc0b  48763  2itscp  48770  inlinecirc02plem  48775  brab2dd  48816  uptr2  49210