MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqcom Structured version   Unicode version

Theorem eqcom 2440
Description: Commutative law for class equality. Theorem 6.5 of [Quine] p. 41. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eqcom  |-  ( A  =  B  <->  B  =  A )

Proof of Theorem eqcom
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 bicom 193 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1576 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2432 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2432 . 2  |-  ( B  =  A  <->  A. x
( x  e.  B  <->  x  e.  A ) )
52, 3, 43bitr4i 270 1  |-  ( A  =  B  <->  B  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1550    = wceq 1653    e. wcel 1726
This theorem is referenced by:  eqcoms  2441  eqcomi  2442  eqcomd  2443  eqeq2  2447  eqtr2  2456  eqtr3  2457  abeq1  2544  nesym  2642  pm13.181  2679  necom  2687  gencbvex  3000  eqsbc3r  3220  dfss  3337  sspsstri  3451  dfss5  3548  disj4  3678  ssnelpss  3693  rabrsn  3876  preqr1  3974  invdisj  4203  disjprg  4210  dtruALT  4398  dtruALT2  4410  opthg2  4439  copsex4g  4447  opcom  4452  opeqsn  4454  opeqpr  4455  opthwiener  4460  ordtri2  4618  suc11  4687  on0eqel  4701  snsn0non  4702  reusv3  4733  onmindif2  4794  opthprc  4927  elxp3  4930  relop  5025  dmopab3  5084  rncoeq  5141  somin1  5272  xpcan  5307  xpcan2  5308  dfrel4v  5324  dmsnn0  5337  iota1  5434  sniota  5447  fresaunres1  5618  dffn5  5774  fvelrnb  5776  dfimafn2  5778  funimass4  5779  fnsnfv  5788  dmfco  5799  fndmdif  5836  fneqeql  5840  rexrn  5874  ralrn  5875  elrnrexdmb  5877  dffo4  5887  ftpg  5918  fconstfv  5956  rexima  5979  ralima  5980  fvclss  5982  dff13  6006  f1eqcocnv  6030  oprabid  6107  eloprabga  6162  ovelimab  6226  dfoprab3  6405  f1o2ndf1  6456  brtpos2  6487  tpossym  6513  opiota  6537  eusvobj2  6584  f1ocnvfv3  6587  rdglim2  6692  tz7.48lem  6700  oaf1o  6808  omopthi  6902  erth2  6952  brecop  6999  erovlem  7002  ecopovsym  7008  eceqoveq  7011  xpcomco  7200  omxpenlem  7211  mapen  7273  nneneq  7292  unxpdomlem3  7317  unfilem1  7373  wemapso2lem  7521  suc11reg  7576  inf3lem2  7586  inf3lem6  7590  mapfien  7655  infenaleph  7974  isinfcard  7975  dfac5  8011  cfeq0  8138  cfsuc  8139  ssfin4  8192  fin23lem25  8206  fin23lem22  8209  fin23lem40  8233  fin1a2lem5  8286  axcclem  8339  brdom7disj  8411  brdom6disj  8412  inar1  8652  psslinpr  8910  ltexprlem4  8918  ltsrpr  8954  mulgt0sr  8982  elreal  9008  ltresr  9017  leloe  9163  eqlei2  9186  addsubeq4  9322  subcan2  9328  negcon1  9355  negcon2  9356  divmul2  9684  conjmul  9733  rereccl  9734  creur  9996  creui  9997  nndiv  10042  nn0sub  10272  elnn0z  10296  elznn0  10298  zq  10582  xrleloe  10739  ngtmnft  10757  icoshftf1o  11022  iccf1o  11041  fzen  11074  4fvwrd4  11123  fzneuz  11130  injresinj  11202  mod0  11257  modirr  11288  nn0ennn  11320  hashsdom  11657  hashgt12el2  11685  hashtpg  11693  hashbclem  11703  hashfacen  11705  hashf1lem1  11706  brfi1uzind  11717  s2f1o  11865  cjreb  11930  leabs  12106  incexc2  12620  rpnnen2  12827  dvdsval2  12857  odd2np1  12910  oddm1even  12911  divalglem4  12918  divalglem8  12922  divalgb  12926  divalgmod  12928  hashdvds  13166  vdwlem12  13362  setcinv  14247  yonedainv  14380  latnle  14516  grpid  14842  grpinvcnv  14861  grplmulf1o  14867  grpsubeq0  14877  grpsubadd  14878  grplactcnv  14889  isnsg4  14985  conjghm  15038  conjnmzb  15042  gacan  15084  gapm  15085  cntzrec  15134  oppgcntz  15162  odmulgeq  15195  dfod2  15202  sylow3lem3  15265  sylow3lem6  15268  lssnle  15308  lsmhash  15339  efgredlemb  15380  efgrelexlemb  15384  dprd2d2  15604  ablfac1eulem  15632  pgpfac1lem2  15635  pgpfac1lem4  15638  dvdsrval  15752  dvdsr02  15763  lvecinv  16187  rspsn  16327  psrbagconf1o  16441  mplmonmul  16529  prmirredlem  16775  zndvds  16832  znleval  16837  istps2OLD  16988  cmpfi  17473  qtopeu  17750  hmeoimaf1o  17804  txhmeo  17837  fbasrn  17918  rnelfmlem  17986  hauspwpwf1  18021  alexsubALTlem4  18083  divstgpopn  18151  divstgphaus  18154  fmucndlem  18323  isngp3  18647  isngp4  18660  metnrmlem1a  18890  icopnfcnv  18969  iccpnfcnv  18971  ivthle  19355  ivthle2  19356  dyadmbl  19494  mbfinf  19559  i1fmulclem  19596  itg1mulc  19598  mvth  19878  dvivth  19896  lhop2  19901  dvdsq1p  20085  reeff1o  20365  coseq1  20432  recosf1o  20439  resinf1o  20440  efopn  20551  cxpeq  20643  logreclem  20662  affineequiv  20669  quad2  20681  dcubic  20688  mcubic  20689  quart  20703  atandm2  20719  rlimcnp2  20807  amgm  20831  wilthlem2  20854  mumullem2  20965  sqff1o  20967  dvdsflip  20969  dvdsflf1o  20974  lgseisenlem2  21136  lgsquadlem2  21141  nbgraop1  21439  nbgraf1olem1  21453  nbgraf1olem5  21457  nbcusgra  21474  fargshiftfo  21627  eupatrl  21692  eupath2lem2  21702  isgrpo  21786  isgrp2d  21825  grpodiveq  21846  opidon  21912  nvsubadd  22138  hvsubaddi  22570  hire  22598  shmodsi  22893  omlsilem  22906  chcon1i  22969  chnlei  22989  pjoml3i  23090  cmbr2i  23100  chscllem2  23142  adjsym  23338  eigorthi  23342  dfadj2  23390  adjval2  23396  cnvadj  23397  dmadjrnb  23411  adjvalval  23442  cnlnadjeui  23582  cnlnssadj  23585  adjbdln  23588  pjimai  23681  pjin2i  23698  pjin3i  23699  stadd3i  23753  largei  23772  cvnbtwn3  23793  cvnbtwn4  23794  mddmd2  23814  superpos  23859  atnemeq0  23882  sumdmdii  23920  sumdmdlem  23923  addltmulALT  23951  difeq  24000  disjrdx  24033  dfimafnf  24045  mptfnf  24075  feqmptdf  24077  funcnvmptOLD  24084  funcnvmpt  24085  curry2ima  24099  addeq0  24116  elicoelioo  24143  ofldsqr  24242  xrmulc1cn  24318  xrge0iifcnv  24321  ind1a  24420  esumfsup  24462  esumpcvgval  24470  esumcvg  24478  issgon  24508  ballotlemi1  24762  ballotlemsima  24775  subfacp1lem3  24870  subfacp1lem5  24872  erdszelem9  24887  br6  25382  fprb  25399  br1steq  25400  br2ndeq  25401  dfon2lem5  25416  dfon2lem8  25419  soseq  25531  sltval2  25613  sltintdifex  25620  sltres  25621  nofulllem5  25663  brbigcup  25745  dfbigcup2  25746  elfix  25750  ellimits  25757  snelsingles  25769  dfiota3  25770  imageval  25777  brapply  25785  brsuccf  25788  funpartlem  25789  brfullfun  25795  dfrdg4  25797  tfrqfree  25798  altopthbg  25815  altopthc  25818  altopthd  25819  altopelaltxp  25823  colinearalglem2  25848  colinearalg  25851  ax5seglem4  25873  ax5seglem5  25874  axlowdimlem13  25895  axeuclidlem  25903  axeuclid  25904  axcontlem2  25906  axcontlem4  25908  brsegle  26044  outsideofrflx  26063  mblfinlem2  26246  mbfresfi  26255  itg2addnclem2  26259  ftc1anclem3  26284  elicc3  26322  nn0prpw  26328  opnregcld  26335  cldregopn  26336  ssref  26365  fneval  26369  topfneec  26373  fdc  26451  heibor1  26521  0rngo  26639  smprngopr  26664  isfldidl  26680  isfldidl2  26681  elrfirn  26751  isnacs2  26762  isnacs3  26766  fiphp3d  26882  wopprc  27103  islnm2  27155  kercvrlsm  27160  phisum  27497  fgraphopab  27508  fmul01lt1lem2  27693  funressnfv  27970  afvpcfv0  27988  dfafn5a  28002  afvelrnb  28005  afvelrnb0  28006  dfaimafn2  28008  oprabv  28091  wrdlen1  28187  2cshwmod  28279  cshw1  28297  cshwssizelem1a  28301  cshwssizelem3  28304  cshwsiun  28308  uvtxnb  28319  usg2wlkeq  28330  usgra2pthlem1  28336  usgra2pth  28337  wlklniswwlkn2  28370  el2wlkonot  28389  el2spthonot  28390  el2wlkonotot0  28392  frgrawopreg2  28502  frg2woteqm  28510  frgregordn0  28521  opelopab4  28700  eqsbc3rVD  29014  bnj1366  29263  bnj553  29331  bnj964  29376  lcvnbtwn3  29888  lcvexchlem1  29894  lsatnem0  29905  opcon1b  30058  omllaw2N  30104  cmtbr2N  30113  leatb  30152  cvlsupr2  30203  glbconxN  30237  islln3  30369  llnexatN  30380  islpln3  30392  lplnexatN  30422  islvol3  30435  dalem-cly  30530  isline4N  30636  2llnma3r  30647  poml4N  30812  4atex2  30936  4atex2-0bOLDN  30938  cdlemefrs29bpre0  31255  cdlemftr3  31424  cdlemb3  31465  cdlemg17h  31527  cdlemg17pq  31531  cdlemg19  31543  cdlemg21  31545  tendoex  31834  dva1dim  31844  dihglb2  32202  doch11  32233  dochsordN  32234  lcfrlem9  32410  hlhillcs  32821
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431
  Copyright terms: Public domain W3C validator