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

Theorem eqcom 2286
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 )
Dummy variable  x is distinct from all other variables.

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 2278 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2278 . 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 1528    = wceq 1624    e. wcel 1685
This theorem is referenced by:  eqcoms  2287  eqcomi  2288  eqcomd  2289  eqeq2  2293  eqtr2  2302  eqtr3  2303  abeq1  2390  pm13.181  2520  necom  2528  gencbvex  2831  reu7  2961  eqsbc3r  3049  dfss  3168  sspsstri  3279  dfss5  3375  disj4  3504  ssnelpss  3518  preqr1  3787  invdisj  4013  disjprg  4020  disjxun  4022  dtruALT  4206  dtruALT2  4218  opthg2  4246  copsexg  4251  copsex4g  4254  opcom  4259  opeqsn  4261  opeqpr  4262  opthwiener  4267  ordtri2  4426  suc11  4495  on0eqel  4509  snsn0non  4510  reusv3  4541  onmindif2  4602  opthprc  4735  elxp3  4738  opeliunxp  4739  relop  4833  dmopab3  4890  rncoeq  4947  intirr  5060  somin1  5078  xpcan  5111  xpcan2  5112  dfrel4v  5124  dmsnn0  5136  fresaunres1  5379  fvprc  5482  dffn5  5529  fvelrnb  5531  dfimafn2  5533  funimass4  5534  fnsnfv  5543  dmfco  5554  fndmdif  5590  fneqeql  5594  rexrn  5628  ralrn  5629  dffo4  5637  fconstfv  5695  rexima  5718  ralima  5719  fvclss  5721  dff13  5744  f1eqcocnv  5766  f1oiso  5809  oprabid  5843  eloprabga  5895  ovelimab  5959  dfoprab3  6137  brtpos2  6201  tpossym  6227  iota1  6266  sniota  6279  opiota  6283  eusvobj2  6332  f1ocnvfv3  6335  rdglim2  6440  tz7.48lem  6448  oaf1o  6556  omopthi  6650  erth2  6700  brecop  6746  erovlem  6749  ecopovsym  6755  eceqoveq  6758  xpcomco  6947  omxpenlem  6958  mapen  7020  nneneq  7039  unxpdomlem3  7064  unfilem1  7116  wemapso2lem  7260  suc11reg  7315  inf3lem2  7325  inf3lem6  7329  mapfien  7394  infenaleph  7713  isinfcard  7714  dfac5  7750  kmlem15  7785  cfeq0  7877  cfsuc  7878  ssfin4  7931  fin23lem25  7945  fin23lem22  7948  fin23lem40  7972  fin1a2lem5  8025  axcclem  8078  brdom7disj  8151  brdom6disj  8152  inar1  8392  psslinpr  8650  ltexprlem4  8658  ltsrpr  8694  mulgt0sr  8722  elreal  8748  ltresr  8757  leloe  8903  addsubeq4  9061  subcan2  9067  negcon1  9094  negcon2  9095  wloglei  9300  divmul2  9423  conjmul  9472  rereccl  9473  creur  9735  creui  9736  nndiv  9781  arch  9957  nn0sub  10009  elnn0z  10031  elznn0  10033  zq  10317  xrleloe  10473  dflt2  10477  ngtmnft  10491  icoshftf1o  10753  iccf1o  10772  fzen  10805  fzneuz  10857  mod0  10972  modirr  11003  nn0ennn  11035  hashsdom  11357  hashbclem  11384  hashfacen  11386  hashf1lem1  11387  cjreb  11602  leabs  11778  incexc2  12291  rpnnen2  12498  dvdsval2  12528  odd2np1  12581  oddm1even  12582  divalglem4  12589  divalglem8  12593  divalgb  12597  divalgmod  12599  hashdvds  12837  vdwlem12  13033  setcinv  13916  yonedainv  14049  latnle  14185  grpid  14511  grpinvcnv  14530  grplmulf1o  14536  grpsubeq0  14546  grpsubadd  14547  grplactcnv  14558  isnsg4  14654  conjghm  14707  conjnmzb  14711  gacan  14753  gapm  14754  cntzrec  14803  oppgcntz  14831  odmulgeq  14864  dfod2  14871  sylow3lem3  14934  sylow3lem6  14937  lssnle  14977  lsmhash  15008  efgredlemb  15049  efgrelexlemb  15053  dprd2d2  15273  ablfac1eulem  15301  pgpfac1lem2  15304  pgpfac1lem4  15307  dvdsrval  15421  dvdsr02  15432  lvecinv  15860  rspsn  16000  psrbagconf1o  16114  mplmonmul  16202  opsrtoslem1  16219  prmirredlem  16440  zndvds  16497  znleval  16502  istps2OLD  16653  cmpfi  17129  qtopeu  17401  hmeoimaf1o  17455  txhmeo  17488  fbasrn  17573  rnelfmlem  17641  hauspwpwf1  17676  alexsubALTlem4  17738  divstgpopn  17796  divstgphaus  17799  isngp3  18114  isngp4  18127  metnrmlem1a  18356  icopnfcnv  18434  iccpnfcnv  18436  ivthle  18810  ivthle2  18811  iundisj2  18900  dyadmbl  18949  mbfinf  19014  i1fmulclem  19051  itg1mulc  19053  mvth  19333  dvivth  19351  lhop2  19356  ply1divmo  19515  dvdsq1p  19540  reeff1o  19817  coseq1  19884  recosf1o  19891  resinf1o  19892  efopn  19999  cxpeq  20091  logreclem  20110  affineequiv  20117  quad2  20129  dcubic  20136  mcubic  20137  quart  20151  atandm2  20167  rlimcnp2  20255  amgm  20279  wilthlem2  20301  mumullem2  20412  sqff1o  20414  dvdsflip  20416  dvdsflf1o  20421  lgseisenlem2  20583  lgsquadlem2  20588  isgrpo  20855  isgrp2d  20894  grpodiveq  20915  opidon  20981  nvsubadd  21205  hvsubaddi  21637  hire  21665  shmodsi  21960  omlsilem  21973  chcon1i  22036  chnlei  22056  pjoml3i  22157  cmbr2i  22167  chscllem2  22209  adjsym  22405  eigorthi  22409  dfadj2  22457  adjval2  22463  cnvadj  22464  dmadjrnb  22478  adjvalval  22509  cnlnadjeui  22649  cnlnssadj  22652  adjbdln  22655  pjimai  22748  pjin2i  22765  pjin3i  22766  stadd3i  22820  largei  22839  cvnbtwn3  22860  cvnbtwn4  22861  mddmd2  22881  superpos  22926  atnemeq0  22949  sumdmdii  22987  sumdmdlem  22990  addltmulALT  23018  dfimafnf  23034  addeq0  23036  ballotlemi1  23054  ballotlemsima  23067  subfacp1lem3  23117  subfacp1lem5  23119  erdszelem9  23134  eupath2lem2  23306  br6  23517  fprb  23530  br1steq  23531  br2ndeq  23532  dfon2lem5  23544  dfon2lem8  23547  soseq  23655  sltval2  23710  sltintdifex  23717  sltres  23718  axfelem18  23764  axfelem20  23766  axfelem22  23768  brbigcup  23846  dfbigcup2  23847  ellimits  23858  snelsingles  23868  dfiota3  23869  imageval  23876  brapply  23884  brsuccf  23887  brfullfun  23893  dfrdg4  23895  tfrqfree  23896  altopthbg  23909  altopthc  23912  altopthd  23913  altopelaltxp  23917  colinearalglem2  23942  colinearalg  23945  ax5seglem4  23967  ax5seglem5  23968  axlowdimlem13  23989  axeuclidlem  23997  axeuclid  23998  axcontlem2  24000  axcontlem4  24002  brsegle  24138  outsideofrflx  24157  copsexgb  24364  elo  24439  surjsec2  24519  sssu  24540  imtr  24797  cnvtr  25015  dualded  25182  dualcat2  25183  cmpmon  25214  iepiclem  25222  isconc2  25406  lineval4a  25486  hpd  25568  elicc3  25627  nn0prpw  25638  opnregcld  25647  cldregopn  25648  ssref  25682  fneval  25686  topfneec  25690  fdc  25854  heibor1  25933  0rngo  26051  smprngopr  26076  isfldidl  26092  isfldidl2  26093  elrfirn  26169  isnacs2  26180  isnacs3  26184  fiphp3d  26301  wopprc  26522  islnm2  26575  kercvrlsm  26580  phisum  26917  fgraphopab  26928  fmul01lt1lem2  27114  wallispilem4  27216  wallispi2lem1  27219  funressnfv  27364  afvpcfv0  27386  dfafn5a  27399  afvelrnb  27402  afvelrnb0  27403  dfaimafn2  27405  opelopab4  27588  eqsbc3rVD  27884  bnj1366  28129  bnj553  28197  bnj964  28242  lcvnbtwn3  28485  lcvexchlem1  28491  lsatnem0  28502  opcon1b  28655  omllaw2N  28701  cmtbr2N  28710  leatb  28749  cvlsupr2  28800  glbconxN  28834  islln3  28966  llnexatN  28977  islpln3  28989  lplnexatN  29019  islvol3  29032  dalem-cly  29127  isline4N  29233  2llnma3r  29244  poml4N  29409  4atex2  29533  4atex2-0bOLDN  29535  cdlemefrs29bpre0  29852  cdlemftr3  30021  cdlemb3  30062  cdlemg17h  30124  cdlemg17pq  30128  cdlemg19  30140  cdlemg21  30142  tendoex  30431  dva1dim  30441  diarnN  30586  dihglb2  30799  doch11  30830  dochsordN  30831  lcfrlem9  31007  hlhillcs  31418
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-cleq 2277
  Copyright terms: Public domain W3C validator