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

Theorem eqcom 2258
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
StepHypRef Expression
1 bicom 193 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1554 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2250 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2250 . 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 1532    = wceq 1619    e. wcel 1621
This theorem is referenced by:  eqcoms  2259  eqcomi  2260  eqcomd  2261  eqeq2  2265  eqtr2  2274  eqtr3  2275  abeq1  2362  pm13.181  2492  necom  2500  gencbvex  2798  reu7  2928  eqsbc3r  3009  dfss  3128  sspsstri  3239  dfss5  3335  disj4  3464  ssnelpss  3478  preqr1  3746  invdisj  3972  disjprg  3979  disjxun  3981  dtruALT  4165  dtruALT2  4177  opthg2  4205  copsexg  4210  copsex4g  4213  opcom  4218  opeqsn  4220  opeqpr  4221  opthwiener  4226  ordtri2  4385  suc11  4454  on0eqel  4468  snsn0non  4469  reusv3  4500  onmindif2  4561  opthprc  4710  elxp3  4713  opeliunxp  4714  relop  4808  dmopab3  4865  rncoeq  4922  intirr  5035  somin1  5053  xpcan  5086  xpcan2  5087  dfrel4v  5099  dmsnn0  5111  fresaunres1  5338  fvprc  5441  dffn5  5488  fvelrnb  5490  dfimafn2  5492  funimass4  5493  fnsnfv  5502  dmfco  5513  fndmdif  5549  fneqeql  5553  rexrn  5587  ralrn  5588  dffo4  5596  fconstfv  5654  rexima  5677  ralima  5678  fvclss  5680  dff13  5703  f1eqcocnv  5725  f1oiso  5768  oprabid  5802  eloprabga  5854  ovelimab  5918  dfoprab3  6096  brtpos2  6160  tpossym  6186  iota1  6225  sniota  6238  opiota  6242  eusvobj2  6291  f1ocnvfv3  6294  rdglim2  6399  tz7.48lem  6407  oaf1o  6515  omopthi  6609  erth2  6659  brecop  6705  erovlem  6708  ecopovsym  6714  eceqoveq  6717  xpcomco  6906  omxpenlem  6917  mapen  6979  nneneq  6998  unxpdomlem3  7023  unfilem1  7075  wemapso2lem  7219  suc11reg  7274  inf3lem2  7284  inf3lem6  7288  mapfien  7353  infenaleph  7672  isinfcard  7673  dfac5  7709  kmlem15  7744  cfeq0  7836  cfsuc  7837  ssfin4  7890  fin23lem25  7904  fin23lem22  7907  fin23lem40  7931  fin1a2lem5  7984  axcclem  8037  brdom7disj  8110  brdom6disj  8111  inar1  8351  psslinpr  8609  ltexprlem4  8617  ltsrpr  8653  mulgt0sr  8681  elreal  8707  ltresr  8716  leloe  8862  addsubeq4  9020  subcan2  9026  negcon1  9053  negcon2  9054  wloglei  9259  divmul2  9382  conjmul  9431  rereccl  9432  creur  9694  creui  9695  nndiv  9740  arch  9915  nn0sub  9967  elnn0z  9989  elznn0  9991  zq  10275  xrleloe  10431  dflt2  10435  ngtmnft  10449  icoshftf1o  10711  iccf1o  10730  fzen  10763  fzneuz  10815  mod0  10930  modirr  10961  nn0ennn  10993  hashsdom  11315  hashbclem  11341  hashfacen  11343  hashf1lem1  11344  cjreb  11559  leabs  11735  rpnnen2  12452  divides2  12482  odd2np1  12535  oddm1even  12536  divalglem4  12543  divalglem8  12547  divalgb  12551  divalgmod  12553  hashdvds  12791  vdwlem12  12987  setcinv  13870  yonedainv  14003  latnle  14139  grpid  14465  grpinvcnv  14484  grplmulf1o  14490  grpsubeq0  14500  grpsubadd  14501  grplactcnv  14512  isnsg4  14608  conjghm  14661  conjnmzb  14665  gacan  14707  gapm  14708  cntzrec  14757  oppgcntz  14785  odmulgeq  14818  dfod2  14825  sylow3lem3  14888  sylow3lem6  14891  lssnle  14931  lsmhash  14962  efgredlemb  15003  efgrelexlemb  15007  dprd2d2  15227  ablfac1eulem  15255  pgpfac1lem2  15258  pgpfac1lem4  15261  dvdsrval  15375  dvdsr02  15386  lvecinv  15814  rspsn  15954  psrbagconf1o  16068  mplmonmul  16156  opsrtoslem1  16173  prmirredlem  16394  zndvds  16451  znleval  16456  istps2OLD  16607  cmpfi  17083  qtopeu  17355  hmeoimaf1o  17409  txhmeo  17442  fbasrn  17527  rnelfmlem  17595  hauspwpwf1  17630  alexsubALTlem4  17692  divstgpopn  17750  divstgphaus  17753  isngp3  18068  isngp4  18081  metnrmlem1a  18310  icopnfcnv  18388  iccpnfcnv  18390  ivthle  18764  ivthle2  18765  iundisj2  18854  dyadmbl  18903  mbfinf  18968  i1fmulclem  19005  itg1mulc  19007  mvth  19287  dvivth  19305  lhop2  19310  ply1divmo  19469  dvdsq1p  19494  reeff1o  19771  coseq1  19838  recosf1o  19845  resinf1o  19846  efopn  19953  cxpeq  20045  logreclem  20064  affineequiv  20071  quad2  20083  dcubic  20090  mcubic  20091  quart  20105  atandm2  20121  rlimcnp2  20209  amgm  20233  wilthlem2  20255  mumullem2  20366  sqff1o  20368  dvdsflip  20370  dvdsflf1o  20375  lgseisenlem2  20537  lgsquadlem2  20542  isgrpo  20809  isgrp2d  20848  grpodiveq  20869  opidon  20935  nvsubadd  21159  hvsubaddi  21591  hire  21619  shmodsi  21914  omlsilem  21927  chcon1i  21990  chnlei  22010  pjoml3i  22129  cmbr2i  22139  chscllem2  22181  adjsym  22359  eigorthi  22363  dfadj2  22411  adjval2  22417  cnvadj  22418  dmadjrnb  22432  adjvalval  22463  cnlnadjeui  22603  cnlnssadj  22606  adjbdln  22609  pjimai  22702  pjin2i  22719  pjin3i  22720  stadd3i  22774  largei  22793  cvnbtwn3  22814  cvnbtwn4  22815  mddmd2  22835  superpos  22880  atnemeq0  22903  sumdmdii  22941  sumdmdlem  22944  addltmulALT  22972  dfimafnf  22988  addeq0  22990  ballotlemi1  23008  ballotlemsima  23021  subfacp1lem3  23071  subfacp1lem5  23073  erdszelem9  23088  eupath2lem2  23260  br6  23471  fprb  23484  br1steq  23485  br2ndeq  23486  dfon2lem5  23498  dfon2lem8  23501  soseq  23609  sltval2  23664  sltintdifex  23671  sltres  23672  axfelem18  23718  axfelem20  23720  axfelem22  23722  brbigcup  23800  dfbigcup2  23801  ellimits  23812  snelsingles  23822  dfiota3  23823  imageval  23830  brapply  23838  brsuccf  23841  brfullfun  23847  dfrdg4  23849  tfrqfree  23850  altopthbg  23863  altopthc  23866  altopthd  23867  altopelaltxp  23871  colinearalglem2  23896  colinearalg  23899  ax5seglem4  23921  ax5seglem5  23922  axlowdimlem13  23943  axeuclidlem  23951  axeuclid  23952  axcontlem2  23954  axcontlem4  23956  brsegle  24092  outsideofrflx  24111  copsexgb  24318  elo  24393  surjsec2  24473  sssu  24494  imtr  24751  cnvtr  24969  dualded  25136  dualcat2  25137  cmpmon  25168  iepiclem  25176  isconc2  25360  lineval4a  25440  hpd  25522  elicc3  25581  nn0prpw  25592  opnregcld  25601  cldregopn  25602  ssref  25636  fneval  25640  topfneec  25644  fdc  25808  heibor1  25887  0rngo  26005  smprngopr  26030  isfldidl  26046  isfldidl2  26047  elrfirn  26123  isnacs2  26134  isnacs3  26138  fiphp3d  26255  wopprc  26476  islnm2  26529  kercvrlsm  26534  phisum  26871  fgraphopab  26882  fmul01lt1lem2  27069  opelopab4  27354  eqsbc3rVD  27650  bnj1366  27895  bnj553  27963  bnj964  28008  lcvnbtwn3  28369  lcvexchlem1  28375  lsatnem0  28386  opcon1b  28539  omllaw2N  28585  cmtbr2N  28594  leatb  28633  cvlsupr2  28684  glbconxN  28718  islln3  28850  llnexatN  28861  islpln3  28873  lplnexatN  28903  islvol3  28916  dalem-cly  29011  isline4N  29117  2llnma3r  29128  poml4N  29293  4atex2  29417  4atex2-0bOLDN  29419  cdlemefrs29bpre0  29736  cdlemftr3  29905  cdlemb3  29946  cdlemg17h  30008  cdlemg17pq  30012  cdlemg19  30024  cdlemg21  30026  tendoex  30315  dva1dim  30325  diarnN  30470  dihglb2  30683  doch11  30714  dochsordN  30715  lcfrlem9  30891  hlhillcs  31302
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-cleq 2249
  Copyright terms: Public domain W3C validator