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

Theorem eqcom 2255
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 2247 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2247 . 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  2256  eqcomi  2257  eqcomd  2258  eqeq2  2262  eqtr2  2271  eqtr3  2272  abeq1  2355  pm13.181  2485  necom  2493  gencbvex  2768  reu7  2899  eqsbc3r  2978  dfss  3090  sspsstri  3198  disj4  3410  ssnelpss  3424  preqr1  3686  invdisj  3909  disjprg  3916  disjxun  3918  dtruALT  4101  dtruALT2  4113  opthg2  4140  copsexg  4145  copsex4g  4148  opcom  4153  opeqsn  4155  opeqpr  4156  opthwiener  4161  ordtri2  4320  suc11  4387  on0eqel  4401  snsn0non  4402  reusv3  4433  onmindif2  4494  opthprc  4643  elxp3  4646  opeliunxp  4647  relop  4741  dmopab3  4798  rncoeq  4855  intirr  4968  somin1  4986  xpcan  5019  xpcan2  5020  dfrel4v  5032  dmsnn0  5044  fresaunres1  5271  fvprc  5374  dffn5  5420  fvelrnb  5422  dfimafn2  5424  funimass4  5425  fnsnfv  5434  dmfco  5445  fndmdif  5481  fneqeql  5485  rexrn  5519  ralrn  5520  dffo4  5528  fconstfv  5586  rexima  5609  ralima  5610  fvclss  5612  dff13  5635  f1eqcocnv  5657  f1oiso  5700  oprabid  5734  eloprabga  5786  ovelimab  5850  dfoprab3  6028  brtpos2  6092  tpossym  6118  iota1  6157  sniota  6170  opiota  6174  eusvobj2  6223  f1ocnvfv3  6226  rdglim2  6331  tz7.48lem  6339  oaf1o  6447  omopthi  6541  erth2  6591  brecop  6637  erovlem  6640  ecopovsym  6646  eceqoveq  6649  xpcomco  6837  omxpenlem  6848  mapen  6910  nneneq  6929  unxpdomlem3  6954  unfilem1  7006  wemapso2lem  7149  suc11reg  7204  inf3lem2  7214  inf3lem6  7218  mapfien  7283  infenaleph  7602  isinfcard  7603  dfac5  7639  kmlem15  7674  cfeq0  7766  cfsuc  7767  ssfin4  7820  fin23lem25  7834  fin23lem22  7837  fin23lem40  7861  fin1a2lem5  7914  axcclem  7967  brdom7disj  8040  brdom6disj  8041  inar1  8277  psslinpr  8535  ltexprlem4  8543  ltsrpr  8579  mulgt0sr  8607  elreal  8633  ltresr  8642  leloe  8788  addsubeq4  8946  subcan2  8952  negcon1  8979  negcon2  8980  wloglei  9185  divmul2  9308  conjmul  9357  rereccl  9358  creur  9620  creui  9621  nndiv  9666  arch  9841  nn0sub  9893  elnn0z  9915  elznn0  9917  zq  10201  xrleloe  10357  dflt2  10361  ngtmnft  10375  icoshftf1o  10637  iccf1o  10656  fzen  10689  fzneuz  10741  mod0  10856  modirr  10887  nn0ennn  10919  hashsdom  11241  hashbclem  11267  hashfacen  11269  hashf1lem1  11270  cjreb  11485  leabs  11661  rpnnen2  12378  divides2  12408  odd2np1  12461  oddm1even  12462  divalglem4  12469  divalglem8  12473  divalgb  12477  divalgmod  12479  hashdvds  12717  vdwlem12  12913  setcinv  13766  yonedainv  13899  latnle  14035  grpid  14352  grpinvcnv  14371  grplmulf1o  14377  grpsubeq0  14387  grpsubadd  14388  grplactcnv  14399  isnsg4  14495  conjghm  14548  conjnmzb  14552  gacan  14594  gapm  14595  cntzrec  14644  oppgcntz  14672  odmulgeq  14705  dfod2  14712  sylow3lem3  14775  sylow3lem6  14778  lssnle  14818  lsmhash  14849  efgredlemb  14890  efgrelexlemb  14894  dprd2d2  15114  ablfac1eulem  15142  pgpfac1lem2  15145  pgpfac1lem4  15148  dvdsrval  15262  dvdsr02  15273  lvecinv  15701  rspsn  15838  psrbagconf1o  15952  mplmonmul  16040  opsrtoslem1  16057  prmirredlem  16278  zndvds  16335  znleval  16340  istps2OLD  16491  cmpfi  16967  qtopeu  17239  hmeoimaf1o  17293  txhmeo  17326  fbasrn  17411  rnelfmlem  17479  hauspwpwf1  17514  alexsubALTlem4  17576  divstgpopn  17634  divstgphaus  17637  isngp3  17952  isngp4  17965  metnrmlem1a  18194  icopnfcnv  18272  iccpnfcnv  18274  ivthle  18648  ivthle2  18649  iundisj2  18738  dyadmbl  18787  mbfinf  18852  i1fmulclem  18889  itg1mulc  18891  mvth  19171  dvivth  19189  lhop2  19194  ply1divmo  19353  dvdsq1p  19378  reeff1o  19655  coseq1  19722  recosf1o  19729  resinf1o  19730  efopn  19837  logreclem  19860  affineequiv  19867  cxpeq  19965  quad2  19967  dcubic  19974  mcubic  19975  quart  19989  atandm2  20005  rlimcnp2  20093  amgm  20117  wilthlem2  20139  mumullem2  20250  sqff1o  20252  dvdsflip  20254  dvdsflf1o  20259  lgseisenlem2  20421  lgsquadlem2  20426  isgrpo  20693  isgrp2d  20732  grpodiveq  20753  opidon  20819  nvsubadd  21043  hvsubaddi  21475  hire  21503  shmodsi  21798  omlsilem  21811  chcon1i  21874  chnlei  21894  pjoml3i  22013  cmbr2i  22023  chscllem2  22065  adjsym  22243  eigorthi  22247  dfadj2  22295  adjval2  22301  cnvadj  22302  dmadjrnb  22316  adjvalval  22347  cnlnadjeui  22487  cnlnssadj  22490  adjbdln  22493  pjimai  22586  pjin2i  22603  pjin3i  22604  stadd3i  22658  largei  22677  cvnbtwn3  22698  cvnbtwn4  22699  mddmd2  22719  superpos  22764  atnemeq0  22787  sumdmdii  22825  sumdmdlem  22828  addltmulALT  22856  subfacp1lem3  22884  subfacp1lem5  22886  erdszelem9  22901  eupath2lem2  23073  br6  23284  fprb  23297  br1steq  23298  br2ndeq  23299  dfon2lem5  23311  dfon2lem8  23314  soseq  23422  sltval2  23477  sltintdifex  23484  sltres  23485  axfelem18  23531  axfelem20  23533  axfelem22  23535  brbigcup  23613  dfbigcup2  23614  ellimits  23625  snelsingles  23635  dfiota3  23636  imageval  23643  brapply  23651  brsuccf  23654  brfullfun  23660  dfrdg4  23662  tfrqfree  23663  altopthbg  23676  altopthc  23679  altopthd  23680  altopelaltxp  23684  colinearalglem2  23709  colinearalg  23712  ax5seglem4  23734  ax5seglem5  23735  axlowdimlem13  23756  axeuclidlem  23764  axeuclid  23765  axcontlem2  23767  axcontlem4  23769  brsegle  23905  outsideofrflx  23924  copsexgb  24131  elo  24206  surjsec2  24286  sssu  24307  imtr  24564  cnvtr  24782  dualded  24949  dualcat2  24950  cmpmon  24981  iepiclem  24989  isconc2  25173  lineval4a  25253  hpd  25335  elicc3  25394  nn0prpw  25405  opnregcld  25414  cldregopn  25415  ssref  25449  fneval  25453  topfneec  25457  fdc  25621  heibor1  25700  0rngo  25818  smprngopr  25843  isfldidl  25859  isfldidl2  25860  elrfirn  25936  isnacs2  25947  isnacs3  25951  fiphp3d  26068  wopprc  26289  islnm2  26342  kercvrlsm  26347  phisum  26684  fgraphopab  26695  fmul01lt1lem2  26882  opelopab4  27107  eqsbc3rVD  27403  bnj1366  27648  bnj553  27716  bnj964  27761  lcvnbtwn3  28122  lcvexchlem1  28128  lsatnem0  28139  opcon1b  28292  omllaw2N  28338  cmtbr2N  28347  leatb  28386  cvlsupr2  28437  glbconxN  28471  islln3  28603  llnexatN  28614  islpln3  28626  lplnexatN  28656  islvol3  28669  dalem-cly  28764  isline4N  28870  2llnma3r  28881  poml4N  29046  4atex2  29170  4atex2-0bOLDN  29172  cdlemefrs29bpre0  29489  cdlemftr3  29658  cdlemb3  29699  cdlemg17h  29761  cdlemg17pq  29765  cdlemg19  29777  cdlemg21  29779  tendoex  30068  dva1dim  30078  diarnN  30223  dihglb2  30436  doch11  30467  dochsordN  30468  lcfrlem9  30644  hlhillcs  31055
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 2234
This theorem depends on definitions:  df-bi 179  df-cleq 2246
  Copyright terms: Public domain W3C validator