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

Theorem eqcom 2437
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 192 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1575 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2429 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2429 . 2  |-  ( B  =  A  <->  A. x
( x  e.  B  <->  x  e.  A ) )
52, 3, 43bitr4i 269 1  |-  ( A  =  B  <->  B  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eqcoms  2438  eqcomi  2439  eqcomd  2440  eqeq2  2444  eqtr2  2453  eqtr3  2454  abeq1  2541  pm13.181  2671  necom  2679  gencbvex  2990  eqsbc3r  3210  dfss  3327  sspsstri  3441  dfss5  3538  disj4  3668  ssnelpss  3683  rabrsn  3866  preqr1  3964  invdisj  4193  disjprg  4200  dtruALT  4388  dtruALT2  4400  opthg2  4429  copsex4g  4437  opcom  4442  opeqsn  4444  opeqpr  4445  opthwiener  4450  ordtri2  4608  suc11  4677  on0eqel  4691  snsn0non  4692  reusv3  4723  onmindif2  4784  opthprc  4917  elxp3  4920  relop  5015  dmopab3  5074  rncoeq  5131  somin1  5262  xpcan  5297  xpcan2  5298  dfrel4v  5314  dmsnn0  5327  iota1  5424  sniota  5437  fresaunres1  5608  dffn5  5764  fvelrnb  5766  dfimafn2  5768  funimass4  5769  fnsnfv  5778  dmfco  5789  fndmdif  5826  fneqeql  5830  rexrn  5864  ralrn  5865  elrnrexdmb  5867  dffo4  5877  ftpg  5908  fconstfv  5946  rexima  5969  ralima  5970  fvclss  5972  dff13  5996  f1eqcocnv  6020  oprabid  6097  eloprabga  6152  ovelimab  6216  dfoprab3  6395  f1o2ndf1  6446  brtpos2  6477  tpossym  6503  opiota  6527  eusvobj2  6574  f1ocnvfv3  6577  rdglim2  6682  tz7.48lem  6690  oaf1o  6798  omopthi  6892  erth2  6942  brecop  6989  erovlem  6992  ecopovsym  6998  eceqoveq  7001  xpcomco  7190  omxpenlem  7201  mapen  7263  nneneq  7282  unxpdomlem3  7307  unfilem1  7363  wemapso2lem  7511  suc11reg  7566  inf3lem2  7576  inf3lem6  7580  mapfien  7645  infenaleph  7964  isinfcard  7965  dfac5  8001  cfeq0  8128  cfsuc  8129  ssfin4  8182  fin23lem25  8196  fin23lem22  8199  fin23lem40  8223  fin1a2lem5  8276  axcclem  8329  brdom7disj  8401  brdom6disj  8402  inar1  8642  psslinpr  8900  ltexprlem4  8908  ltsrpr  8944  mulgt0sr  8972  elreal  8998  ltresr  9007  leloe  9153  eqlei2  9176  addsubeq4  9312  subcan2  9318  negcon1  9345  negcon2  9346  divmul2  9674  conjmul  9723  rereccl  9724  creur  9986  creui  9987  nndiv  10032  nn0sub  10262  elnn0z  10286  elznn0  10288  zq  10572  xrleloe  10729  ngtmnft  10747  icoshftf1o  11012  iccf1o  11031  fzen  11064  4fvwrd4  11113  fzneuz  11120  injresinj  11192  mod0  11247  modirr  11278  nn0ennn  11310  hashsdom  11647  hashgt12el2  11675  hashtpg  11683  hashbclem  11693  hashfacen  11695  hashf1lem1  11696  brfi1uzind  11707  s2f1o  11855  cjreb  11920  leabs  12096  incexc2  12610  rpnnen2  12817  dvdsval2  12847  odd2np1  12900  oddm1even  12901  divalglem4  12908  divalglem8  12912  divalgb  12916  divalgmod  12918  hashdvds  13156  vdwlem12  13352  setcinv  14237  yonedainv  14370  latnle  14506  grpid  14832  grpinvcnv  14851  grplmulf1o  14857  grpsubeq0  14867  grpsubadd  14868  grplactcnv  14879  isnsg4  14975  conjghm  15028  conjnmzb  15032  gacan  15074  gapm  15075  cntzrec  15124  oppgcntz  15152  odmulgeq  15185  dfod2  15192  sylow3lem3  15255  sylow3lem6  15258  lssnle  15298  lsmhash  15329  efgredlemb  15370  efgrelexlemb  15374  dprd2d2  15594  ablfac1eulem  15622  pgpfac1lem2  15625  pgpfac1lem4  15628  dvdsrval  15742  dvdsr02  15753  lvecinv  16177  rspsn  16317  psrbagconf1o  16431  mplmonmul  16519  prmirredlem  16765  zndvds  16822  znleval  16827  istps2OLD  16978  cmpfi  17463  qtopeu  17740  hmeoimaf1o  17794  txhmeo  17827  fbasrn  17908  rnelfmlem  17976  hauspwpwf1  18011  alexsubALTlem4  18073  divstgpopn  18141  divstgphaus  18144  fmucndlem  18313  isngp3  18637  isngp4  18650  metnrmlem1a  18880  icopnfcnv  18959  iccpnfcnv  18961  ivthle  19345  ivthle2  19346  dyadmbl  19484  mbfinf  19549  i1fmulclem  19586  itg1mulc  19588  mvth  19868  dvivth  19886  lhop2  19891  dvdsq1p  20075  reeff1o  20355  coseq1  20422  recosf1o  20429  resinf1o  20430  efopn  20541  cxpeq  20633  logreclem  20652  affineequiv  20659  quad2  20671  dcubic  20678  mcubic  20679  quart  20693  atandm2  20709  rlimcnp2  20797  amgm  20821  wilthlem2  20844  mumullem2  20955  sqff1o  20957  dvdsflip  20959  dvdsflf1o  20964  lgseisenlem2  21126  lgsquadlem2  21131  nbgraop1  21429  nbgraf1olem1  21443  nbgraf1olem5  21447  nbcusgra  21464  fargshiftfo  21617  eupatrl  21682  eupath2lem2  21692  isgrpo  21776  isgrp2d  21815  grpodiveq  21836  opidon  21902  nvsubadd  22128  hvsubaddi  22560  hire  22588  shmodsi  22883  omlsilem  22896  chcon1i  22959  chnlei  22979  pjoml3i  23080  cmbr2i  23090  chscllem2  23132  adjsym  23328  eigorthi  23332  dfadj2  23380  adjval2  23386  cnvadj  23387  dmadjrnb  23401  adjvalval  23432  cnlnadjeui  23572  cnlnssadj  23575  adjbdln  23578  pjimai  23671  pjin2i  23688  pjin3i  23689  stadd3i  23743  largei  23762  cvnbtwn3  23783  cvnbtwn4  23784  mddmd2  23804  superpos  23849  atnemeq0  23872  sumdmdii  23910  sumdmdlem  23913  addltmulALT  23941  difeq  23990  disjrdx  24023  dfimafnf  24035  mptfnf  24065  feqmptdf  24067  funcnvmptOLD  24074  funcnvmpt  24075  curry2ima  24089  addeq0  24106  elicoelioo  24133  ofldsqr  24232  xrmulc1cn  24308  xrge0iifcnv  24311  ind1a  24410  esumfsup  24452  esumpcvgval  24460  esumcvg  24468  issgon  24498  ballotlemi1  24752  ballotlemsima  24765  subfacp1lem3  24860  subfacp1lem5  24862  erdszelem9  24877  br6  25372  fprb  25389  br1steq  25390  br2ndeq  25391  dfon2lem5  25406  dfon2lem8  25409  soseq  25521  sltval2  25603  sltintdifex  25610  sltres  25611  nofulllem5  25653  brbigcup  25735  dfbigcup2  25736  elfix  25740  ellimits  25747  snelsingles  25759  dfiota3  25760  imageval  25767  brapply  25775  brsuccf  25778  funpartlem  25779  brfullfun  25785  dfrdg4  25787  tfrqfree  25788  altopthbg  25805  altopthc  25808  altopthd  25809  altopelaltxp  25813  colinearalglem2  25838  colinearalg  25841  ax5seglem4  25863  ax5seglem5  25864  axlowdimlem13  25885  axeuclidlem  25893  axeuclid  25894  axcontlem2  25896  axcontlem4  25898  brsegle  26034  outsideofrflx  26053  mblfinlem  26234  mbfresfi  26243  itg2addnclem2  26247  ftc1anclem3  26272  elicc3  26311  nn0prpw  26317  opnregcld  26324  cldregopn  26325  ssref  26354  fneval  26358  topfneec  26362  fdc  26440  heibor1  26510  0rngo  26628  smprngopr  26653  isfldidl  26669  isfldidl2  26670  elrfirn  26740  isnacs2  26751  isnacs3  26755  fiphp3d  26871  wopprc  27092  islnm2  27144  kercvrlsm  27149  phisum  27486  fgraphopab  27497  fmul01lt1lem2  27682  funressnfv  27959  afvpcfv0  27977  dfafn5a  27991  afvelrnb  27994  afvelrnb0  27995  dfaimafn2  27997  2cshwmod  28223  cshw1  28238  cshwssizelem1a  28242  cshwssizelem3  28245  cshwsiun  28249  usgra2pthlem1  28263  usgra2pth  28264  el2wlkonot  28289  el2spthonot  28290  el2wlkonotot0  28292  frgrawopreg2  28377  frg2woteqm  28385  frgregordn0  28396  opelopab4  28575  eqsbc3rVD  28889  bnj1366  29138  bnj553  29206  bnj964  29251  lcvnbtwn3  29763  lcvexchlem1  29769  lsatnem0  29780  opcon1b  29933  omllaw2N  29979  cmtbr2N  29988  leatb  30027  cvlsupr2  30078  glbconxN  30112  islln3  30244  llnexatN  30255  islpln3  30267  lplnexatN  30297  islvol3  30310  dalem-cly  30405  isline4N  30511  2llnma3r  30522  poml4N  30687  4atex2  30811  4atex2-0bOLDN  30813  cdlemefrs29bpre0  31130  cdlemftr3  31299  cdlemb3  31340  cdlemg17h  31402  cdlemg17pq  31406  cdlemg19  31418  cdlemg21  31420  tendoex  31709  dva1dim  31719  dihglb2  32077  doch11  32108  dochsordN  32109  lcfrlem9  32285  hlhillcs  32696
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-cleq 2428
  Copyright terms: Public domain W3C validator