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

Theorem eqcom 2406
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 1572 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2398 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2398 . 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 1546    = wceq 1649    e. wcel 1721
This theorem is referenced by:  eqcoms  2407  eqcomi  2408  eqcomd  2409  eqeq2  2413  eqtr2  2422  eqtr3  2423  abeq1  2510  pm13.181  2640  necom  2648  gencbvex  2958  eqsbc3r  3178  dfss  3295  sspsstri  3409  dfss5  3506  disj4  3636  ssnelpss  3651  rabrsn  3834  preqr1  3932  invdisj  4161  disjprg  4168  dtruALT  4356  dtruALT2  4368  opthg2  4397  copsex4g  4405  opcom  4410  opeqsn  4412  opeqpr  4413  opthwiener  4418  ordtri2  4576  suc11  4644  on0eqel  4658  snsn0non  4659  reusv3  4690  onmindif2  4751  opthprc  4884  elxp3  4887  relop  4982  dmopab3  5041  rncoeq  5098  somin1  5229  xpcan  5264  xpcan2  5265  dfrel4v  5281  dmsnn0  5294  iota1  5391  sniota  5404  fresaunres1  5575  dffn5  5731  fvelrnb  5733  dfimafn2  5735  funimass4  5736  fnsnfv  5745  dmfco  5756  fndmdif  5793  fneqeql  5797  rexrn  5831  ralrn  5832  elrnrexdmb  5834  dffo4  5844  ftpg  5875  fconstfv  5913  rexima  5936  ralima  5937  fvclss  5939  dff13  5963  f1eqcocnv  5987  oprabid  6064  eloprabga  6119  ovelimab  6183  dfoprab3  6362  f1o2ndf1  6413  brtpos2  6444  tpossym  6470  opiota  6494  eusvobj2  6541  f1ocnvfv3  6544  rdglim2  6649  tz7.48lem  6657  oaf1o  6765  omopthi  6859  erth2  6909  brecop  6956  erovlem  6959  ecopovsym  6965  eceqoveq  6968  xpcomco  7157  omxpenlem  7168  mapen  7230  nneneq  7249  unxpdomlem3  7274  unfilem1  7330  wemapso2lem  7475  suc11reg  7530  inf3lem2  7540  inf3lem6  7544  mapfien  7609  infenaleph  7928  isinfcard  7929  dfac5  7965  cfeq0  8092  cfsuc  8093  ssfin4  8146  fin23lem25  8160  fin23lem22  8163  fin23lem40  8187  fin1a2lem5  8240  axcclem  8293  brdom7disj  8365  brdom6disj  8366  inar1  8606  psslinpr  8864  ltexprlem4  8872  ltsrpr  8908  mulgt0sr  8936  elreal  8962  ltresr  8971  leloe  9117  eqlei2  9140  addsubeq4  9276  subcan2  9282  negcon1  9309  negcon2  9310  divmul2  9638  conjmul  9687  rereccl  9688  creur  9950  creui  9951  nndiv  9996  nn0sub  10226  elnn0z  10250  elznn0  10252  zq  10536  xrleloe  10693  ngtmnft  10711  icoshftf1o  10976  iccf1o  10995  fzen  11028  4fvwrd4  11076  fzneuz  11083  injresinj  11155  mod0  11210  modirr  11241  nn0ennn  11273  hashsdom  11610  hashgt12el2  11638  hashtpg  11646  hashbclem  11656  hashfacen  11658  hashf1lem1  11659  brfi1uzind  11670  s2f1o  11818  cjreb  11883  leabs  12059  incexc2  12573  rpnnen2  12780  dvdsval2  12810  odd2np1  12863  oddm1even  12864  divalglem4  12871  divalglem8  12875  divalgb  12879  divalgmod  12881  hashdvds  13119  vdwlem12  13315  setcinv  14200  yonedainv  14333  latnle  14469  grpid  14795  grpinvcnv  14814  grplmulf1o  14820  grpsubeq0  14830  grpsubadd  14831  grplactcnv  14842  isnsg4  14938  conjghm  14991  conjnmzb  14995  gacan  15037  gapm  15038  cntzrec  15087  oppgcntz  15115  odmulgeq  15148  dfod2  15155  sylow3lem3  15218  sylow3lem6  15221  lssnle  15261  lsmhash  15292  efgredlemb  15333  efgrelexlemb  15337  dprd2d2  15557  ablfac1eulem  15585  pgpfac1lem2  15588  pgpfac1lem4  15591  dvdsrval  15705  dvdsr02  15716  lvecinv  16140  rspsn  16280  psrbagconf1o  16394  mplmonmul  16482  prmirredlem  16728  zndvds  16785  znleval  16790  istps2OLD  16941  cmpfi  17425  qtopeu  17701  hmeoimaf1o  17755  txhmeo  17788  fbasrn  17869  rnelfmlem  17937  hauspwpwf1  17972  alexsubALTlem4  18034  divstgpopn  18102  divstgphaus  18105  fmucndlem  18274  isngp3  18598  isngp4  18611  metnrmlem1a  18841  icopnfcnv  18920  iccpnfcnv  18922  ivthle  19306  ivthle2  19307  dyadmbl  19445  mbfinf  19510  i1fmulclem  19547  itg1mulc  19549  mvth  19829  dvivth  19847  lhop2  19852  dvdsq1p  20036  reeff1o  20316  coseq1  20383  recosf1o  20390  resinf1o  20391  efopn  20502  cxpeq  20594  logreclem  20613  affineequiv  20620  quad2  20632  dcubic  20639  mcubic  20640  quart  20654  atandm2  20670  rlimcnp2  20758  amgm  20782  wilthlem2  20805  mumullem2  20916  sqff1o  20918  dvdsflip  20920  dvdsflf1o  20925  lgseisenlem2  21087  lgsquadlem2  21092  nbgraop1  21390  nbgraf1olem1  21404  nbgraf1olem5  21408  nbcusgra  21425  fargshiftfo  21578  eupatrl  21643  eupath2lem2  21653  isgrpo  21737  isgrp2d  21776  grpodiveq  21797  opidon  21863  nvsubadd  22089  hvsubaddi  22521  hire  22549  shmodsi  22844  omlsilem  22857  chcon1i  22920  chnlei  22940  pjoml3i  23041  cmbr2i  23051  chscllem2  23093  adjsym  23289  eigorthi  23293  dfadj2  23341  adjval2  23347  cnvadj  23348  dmadjrnb  23362  adjvalval  23393  cnlnadjeui  23533  cnlnssadj  23536  adjbdln  23539  pjimai  23632  pjin2i  23649  pjin3i  23650  stadd3i  23704  largei  23723  cvnbtwn3  23744  cvnbtwn4  23745  mddmd2  23765  superpos  23810  atnemeq0  23833  sumdmdii  23871  sumdmdlem  23874  addltmulALT  23902  difeq  23951  disjrdx  23984  dfimafnf  23996  mptfnf  24026  feqmptdf  24028  funcnvmptOLD  24035  funcnvmpt  24036  curry2ima  24050  addeq0  24067  elicoelioo  24094  ofldsqr  24193  xrmulc1cn  24269  xrge0iifcnv  24272  ind1a  24371  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  issgon  24459  ballotlemi1  24713  ballotlemsima  24726  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem9  24838  br6  25328  fprb  25343  br1steq  25344  br2ndeq  25345  dfon2lem5  25357  dfon2lem8  25360  soseq  25468  sltval2  25524  sltintdifex  25531  sltres  25532  nofulllem5  25574  brbigcup  25652  dfbigcup2  25653  ellimits  25664  elfuns  25668  snelsingles  25675  dfiota3  25676  imageval  25683  brapply  25691  brsuccf  25694  funpartlem  25695  brfullfun  25701  dfrdg4  25703  tfrqfree  25704  altopthbg  25717  altopthc  25720  altopthd  25721  altopelaltxp  25725  colinearalglem2  25750  colinearalg  25753  ax5seglem4  25775  ax5seglem5  25776  axlowdimlem13  25797  axeuclidlem  25805  axeuclid  25806  axcontlem2  25808  axcontlem4  25810  brsegle  25946  outsideofrflx  25965  mblfinlem  26143  mbfresfi  26152  itg2addnclem2  26156  elicc3  26210  nn0prpw  26216  opnregcld  26223  cldregopn  26224  ssref  26253  fneval  26257  topfneec  26261  fdc  26339  heibor1  26409  0rngo  26527  smprngopr  26552  isfldidl  26568  isfldidl2  26569  elrfirn  26639  isnacs2  26650  isnacs3  26654  fiphp3d  26770  wopprc  26991  islnm2  27044  kercvrlsm  27049  phisum  27386  fgraphopab  27397  fmul01lt1lem2  27582  funressnfv  27859  afvpcfv0  27877  dfafn5a  27891  afvelrnb  27894  afvelrnb0  27895  dfaimafn2  27897  swrdccat3b  28031  usgra2pthlem1  28040  usgra2pth  28041  el2wlkonot  28066  el2spthonot  28067  el2wlkonotot0  28069  frgrawopreg2  28154  frg2woteqm  28162  frgregordn0  28173  opelopab4  28349  eqsbc3rVD  28661  bnj1366  28907  bnj553  28975  bnj964  29020  lcvnbtwn3  29511  lcvexchlem1  29517  lsatnem0  29528  opcon1b  29681  omllaw2N  29727  cmtbr2N  29736  leatb  29775  cvlsupr2  29826  glbconxN  29860  islln3  29992  llnexatN  30003  islpln3  30015  lplnexatN  30045  islvol3  30058  dalem-cly  30153  isline4N  30259  2llnma3r  30270  poml4N  30435  4atex2  30559  4atex2-0bOLDN  30561  cdlemefrs29bpre0  30878  cdlemftr3  31047  cdlemb3  31088  cdlemg17h  31150  cdlemg17pq  31154  cdlemg19  31166  cdlemg21  31168  tendoex  31457  dva1dim  31467  dihglb2  31825  doch11  31856  dochsordN  31857  lcfrlem9  32033  hlhillcs  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-cleq 2397
  Copyright terms: Public domain W3C validator