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  4204  disjprg  4211  dtruALT  4399  dtruALT2  4411  opthg2  4440  copsex4g  4448  opcom  4453  opeqsn  4455  opeqpr  4456  opthwiener  4461  ordtri2  4619  suc11  4688  on0eqel  4702  snsn0non  4703  reusv3  4734  onmindif2  4795  opthprc  4928  elxp3  4931  relop  5026  dmopab3  5085  rncoeq  5142  somin1  5273  xpcan  5308  xpcan2  5309  dfrel4v  5325  dmsnn0  5338  iota1  5435  sniota  5448  fresaunres1  5619  dffn5  5775  fvelrnb  5777  dfimafn2  5779  funimass4  5780  fnsnfv  5789  dmfco  5800  fndmdif  5837  fneqeql  5841  rexrn  5875  ralrn  5876  elrnrexdmb  5878  dffo4  5888  ftpg  5919  fconstfv  5957  rexima  5980  ralima  5981  fvclss  5983  dff13  6007  f1eqcocnv  6031  oprabid  6108  eloprabga  6163  ovelimab  6227  dfoprab3  6406  f1o2ndf1  6457  brtpos2  6488  tpossym  6514  opiota  6538  eusvobj2  6585  f1ocnvfv3  6588  rdglim2  6693  tz7.48lem  6701  oaf1o  6809  omopthi  6903  erth2  6953  brecop  7000  erovlem  7003  ecopovsym  7009  eceqoveq  7012  xpcomco  7201  omxpenlem  7212  mapen  7274  nneneq  7293  unxpdomlem3  7318  unfilem1  7374  wemapso2lem  7522  suc11reg  7577  inf3lem2  7587  inf3lem6  7591  mapfien  7656  infenaleph  7977  isinfcard  7978  dfac5  8014  cfeq0  8141  cfsuc  8142  ssfin4  8195  fin23lem25  8209  fin23lem22  8212  fin23lem40  8236  fin1a2lem5  8289  axcclem  8342  brdom7disj  8414  brdom6disj  8415  inar1  8655  psslinpr  8913  ltexprlem4  8921  ltsrpr  8957  mulgt0sr  8985  elreal  9011  ltresr  9020  leloe  9166  eqlei2  9189  addsubeq4  9325  subcan2  9331  negcon1  9358  negcon2  9359  divmul2  9687  conjmul  9736  rereccl  9737  creur  9999  creui  10000  nndiv  10045  nn0sub  10275  elnn0z  10299  elznn0  10301  zq  10585  xrleloe  10742  ngtmnft  10760  icoshftf1o  11025  iccf1o  11044  fzen  11077  4fvwrd4  11126  fzneuz  11133  injresinj  11205  mod0  11260  modirr  11291  nn0ennn  11323  hashsdom  11660  hashgt12el2  11688  hashtpg  11696  hashbclem  11706  hashfacen  11708  hashf1lem1  11709  brfi1uzind  11720  s2f1o  11868  cjreb  11933  leabs  12109  incexc2  12623  rpnnen2  12830  dvdsval2  12860  odd2np1  12913  oddm1even  12914  divalglem4  12921  divalglem8  12925  divalgb  12929  divalgmod  12931  hashdvds  13169  vdwlem12  13365  setcinv  14250  yonedainv  14383  latnle  14519  grpid  14845  grpinvcnv  14864  grplmulf1o  14870  grpsubeq0  14880  grpsubadd  14881  grplactcnv  14892  isnsg4  14988  conjghm  15041  conjnmzb  15045  gacan  15087  gapm  15088  cntzrec  15137  oppgcntz  15165  odmulgeq  15198  dfod2  15205  sylow3lem3  15268  sylow3lem6  15271  lssnle  15311  lsmhash  15342  efgredlemb  15383  efgrelexlemb  15387  dprd2d2  15607  ablfac1eulem  15635  pgpfac1lem2  15638  pgpfac1lem4  15641  dvdsrval  15755  dvdsr02  15766  lvecinv  16190  rspsn  16330  psrbagconf1o  16444  mplmonmul  16532  prmirredlem  16778  zndvds  16835  znleval  16840  istps2OLD  16991  cmpfi  17476  qtopeu  17753  hmeoimaf1o  17807  txhmeo  17840  fbasrn  17921  rnelfmlem  17989  hauspwpwf1  18024  alexsubALTlem4  18086  divstgpopn  18154  divstgphaus  18157  fmucndlem  18326  isngp3  18650  isngp4  18663  metnrmlem1a  18893  icopnfcnv  18972  iccpnfcnv  18974  ivthle  19358  ivthle2  19359  dyadmbl  19497  mbfinf  19560  i1fmulclem  19597  itg1mulc  19599  mvth  19881  dvivth  19899  lhop2  19904  dvdsq1p  20088  reeff1o  20368  coseq1  20435  recosf1o  20442  resinf1o  20443  efopn  20554  cxpeq  20646  logreclem  20665  affineequiv  20672  quad2  20684  dcubic  20691  mcubic  20692  quart  20706  atandm2  20722  rlimcnp2  20810  amgm  20834  wilthlem2  20857  mumullem2  20968  sqff1o  20970  dvdsflip  20972  dvdsflf1o  20977  lgseisenlem2  21139  lgsquadlem2  21144  nbgraop1  21442  nbgraf1olem1  21456  nbgraf1olem5  21460  nbcusgra  21477  fargshiftfo  21630  eupatrl  21695  eupath2lem2  21705  isgrpo  21789  isgrp2d  21828  grpodiveq  21849  opidon  21915  nvsubadd  22141  hvsubaddi  22573  hire  22601  shmodsi  22896  omlsilem  22909  chcon1i  22972  chnlei  22992  pjoml3i  23093  cmbr2i  23103  chscllem2  23145  adjsym  23341  eigorthi  23345  dfadj2  23393  adjval2  23399  cnvadj  23400  dmadjrnb  23414  adjvalval  23445  cnlnadjeui  23585  cnlnssadj  23588  adjbdln  23591  pjimai  23684  pjin2i  23701  pjin3i  23702  stadd3i  23756  largei  23775  cvnbtwn3  23796  cvnbtwn4  23797  mddmd2  23817  superpos  23862  atnemeq0  23885  sumdmdii  23923  sumdmdlem  23926  addltmulALT  23954  difeq  24003  disjrdx  24036  dfimafnf  24048  mptfnf  24078  feqmptdf  24080  funcnvmptOLD  24087  funcnvmpt  24088  curry2ima  24102  addeq0  24119  elicoelioo  24146  ofldsqr  24245  xrmulc1cn  24321  xrge0iifcnv  24324  ind1a  24423  esumfsup  24465  esumpcvgval  24473  esumcvg  24481  issgon  24511  ballotlemi1  24765  ballotlemsima  24778  subfacp1lem3  24873  subfacp1lem5  24875  erdszelem9  24890  br6  25385  fprb  25402  br1steq  25403  br2ndeq  25404  dfon2lem5  25419  dfon2lem8  25422  soseq  25534  sltval2  25616  sltintdifex  25623  sltres  25624  nofulllem5  25666  brbigcup  25748  dfbigcup2  25749  elfix  25753  ellimits  25760  snelsingles  25772  dfiota3  25773  imageval  25780  brapply  25788  brsuccf  25791  funpartlem  25792  brfullfun  25798  dfrdg4  25800  tfrqfree  25801  altopthbg  25818  altopthc  25821  altopthd  25822  altopelaltxp  25826  colinearalglem2  25851  colinearalg  25854  ax5seglem4  25876  ax5seglem5  25877  axlowdimlem13  25898  axeuclidlem  25906  axeuclid  25907  axcontlem2  25909  axcontlem4  25911  brsegle  26047  outsideofrflx  26066  mblfinlem2  26256  mbfresfi  26265  itg2addnclem2  26271  ftc1anclem3  26296  elicc3  26334  nn0prpw  26340  opnregcld  26347  cldregopn  26348  ssref  26377  fneval  26381  topfneec  26385  fdc  26463  heibor1  26533  0rngo  26651  smprngopr  26676  isfldidl  26692  isfldidl2  26693  elrfirn  26763  isnacs2  26774  isnacs3  26778  fiphp3d  26894  wopprc  27115  islnm2  27167  kercvrlsm  27172  phisum  27509  fgraphopab  27520  fmul01lt1lem2  27705  funressnfv  27982  afvpcfv0  28000  dfafn5a  28014  afvelrnb  28017  afvelrnb0  28018  dfaimafn2  28020  oprabv  28103  wrdlen1  28199  2cshwmod  28291  cshw1  28309  cshwssizelem1a  28313  cshwssizelem3  28316  cshwsiun  28320  uvtxnb  28331  usg2wlkeq  28342  usgra2pthlem1  28348  usgra2pth  28349  wlklniswwlkn2  28382  el2wlkonot  28401  el2spthonot  28402  el2wlkonotot0  28404  frgrawopreg2  28514  frg2woteqm  28522  frgregordn0  28533  opelopab4  28712  eqsbc3rVD  29026  bnj1366  29275  bnj553  29343  bnj964  29388  lcvnbtwn3  29900  lcvexchlem1  29906  lsatnem0  29917  opcon1b  30070  omllaw2N  30116  cmtbr2N  30125  leatb  30164  cvlsupr2  30215  glbconxN  30249  islln3  30381  llnexatN  30392  islpln3  30404  lplnexatN  30434  islvol3  30447  dalem-cly  30542  isline4N  30648  2llnma3r  30659  poml4N  30824  4atex2  30948  4atex2-0bOLDN  30950  cdlemefrs29bpre0  31267  cdlemftr3  31436  cdlemb3  31477  cdlemg17h  31539  cdlemg17pq  31543  cdlemg19  31555  cdlemg21  31557  tendoex  31846  dva1dim  31856  dihglb2  32214  doch11  32245  dochsordN  32246  lcfrlem9  32422  hlhillcs  32833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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