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

Theorem eqcom 2285
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 191 . . 3  |-  ( ( x  e.  A  <->  x  e.  B )  <->  ( x  e.  B  <->  x  e.  A
) )
21albii 1553 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2277 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2277 . 2  |-  ( B  =  A  <->  A. x
( x  e.  B  <->  x  e.  A ) )
52, 3, 43bitr4i 268 1  |-  ( A  =  B  <->  B  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527    = wceq 1623    e. wcel 1684
This theorem is referenced by:  eqcoms  2286  eqcomi  2287  eqcomd  2288  eqeq2  2292  eqtr2  2301  eqtr3  2302  abeq1  2389  pm13.181  2519  necom  2527  gencbvex  2830  reu7  2960  eqsbc3r  3048  dfss  3167  sspsstri  3278  dfss5  3374  disj4  3503  ssnelpss  3517  preqr1  3786  invdisj  4012  disjprg  4019  disjxun  4021  dtruALT  4207  dtruALT2  4219  opthg2  4247  copsexg  4252  copsex4g  4255  opcom  4260  opeqsn  4262  opeqpr  4263  opthwiener  4268  ordtri2  4427  suc11  4496  on0eqel  4510  snsn0non  4511  reusv3  4542  onmindif2  4603  opthprc  4736  elxp3  4739  opeliunxp  4740  relop  4834  dmopab3  4891  rncoeq  4948  intirr  5061  somin1  5079  xpcan  5112  xpcan2  5113  dfrel4v  5125  dmsnn0  5138  iota1  5233  sniota  5246  fresaunres1  5414  dffn5  5568  fvelrnb  5570  dfimafn2  5572  funimass4  5573  fnsnfv  5582  dmfco  5593  fndmdif  5629  fneqeql  5633  rexrn  5667  ralrn  5668  dffo4  5676  fconstfv  5734  rexima  5757  ralima  5758  fvclss  5760  dff13  5783  f1eqcocnv  5805  f1oiso  5848  oprabid  5882  eloprabga  5934  ovelimab  5998  dfoprab3  6176  brtpos2  6240  tpossym  6266  opiota  6290  eusvobj2  6337  f1ocnvfv3  6340  rdglim2  6445  tz7.48lem  6453  oaf1o  6561  omopthi  6655  erth2  6705  brecop  6751  erovlem  6754  ecopovsym  6760  eceqoveq  6763  xpcomco  6952  omxpenlem  6963  mapen  7025  nneneq  7044  unxpdomlem3  7069  unfilem1  7121  wemapso2lem  7265  suc11reg  7320  inf3lem2  7330  inf3lem6  7334  mapfien  7399  infenaleph  7718  isinfcard  7719  dfac5  7755  kmlem15  7790  cfeq0  7882  cfsuc  7883  ssfin4  7936  fin23lem25  7950  fin23lem22  7953  fin23lem40  7977  fin1a2lem5  8030  axcclem  8083  brdom7disj  8156  brdom6disj  8157  inar1  8397  psslinpr  8655  ltexprlem4  8663  ltsrpr  8699  mulgt0sr  8727  elreal  8753  ltresr  8762  leloe  8908  addsubeq4  9066  subcan2  9072  negcon1  9099  negcon2  9100  wloglei  9305  divmul2  9428  conjmul  9477  rereccl  9478  creur  9740  creui  9741  nndiv  9786  arch  9962  nn0sub  10014  elnn0z  10036  elznn0  10038  zq  10322  xrleloe  10478  dflt2  10482  ngtmnft  10496  icoshftf1o  10759  iccf1o  10778  fzen  10811  fzneuz  10863  mod0  10978  modirr  11009  nn0ennn  11041  hashsdom  11363  hashbclem  11390  hashfacen  11392  hashf1lem1  11393  cjreb  11608  leabs  11784  incexc2  12297  rpnnen2  12504  dvdsval2  12534  odd2np1  12587  oddm1even  12588  divalglem4  12595  divalglem8  12599  divalgb  12603  divalgmod  12605  hashdvds  12843  vdwlem12  13039  setcinv  13922  yonedainv  14055  latnle  14191  grpid  14517  grpinvcnv  14536  grplmulf1o  14542  grpsubeq0  14552  grpsubadd  14553  grplactcnv  14564  isnsg4  14660  conjghm  14713  conjnmzb  14717  gacan  14759  gapm  14760  cntzrec  14809  oppgcntz  14837  odmulgeq  14870  dfod2  14877  sylow3lem3  14940  sylow3lem6  14943  lssnle  14983  lsmhash  15014  efgredlemb  15055  efgrelexlemb  15059  dprd2d2  15279  ablfac1eulem  15307  pgpfac1lem2  15310  pgpfac1lem4  15313  dvdsrval  15427  dvdsr02  15438  lvecinv  15866  rspsn  16006  psrbagconf1o  16120  mplmonmul  16208  opsrtoslem1  16225  prmirredlem  16446  zndvds  16503  znleval  16508  istps2OLD  16659  cmpfi  17135  qtopeu  17407  hmeoimaf1o  17461  txhmeo  17494  fbasrn  17579  rnelfmlem  17647  hauspwpwf1  17682  alexsubALTlem4  17744  divstgpopn  17802  divstgphaus  17805  isngp3  18120  isngp4  18133  metnrmlem1a  18362  icopnfcnv  18440  iccpnfcnv  18442  ivthle  18816  ivthle2  18817  iundisj2  18906  dyadmbl  18955  mbfinf  19020  i1fmulclem  19057  itg1mulc  19059  mvth  19339  dvivth  19357  lhop2  19362  ply1divmo  19521  dvdsq1p  19546  reeff1o  19823  coseq1  19890  recosf1o  19897  resinf1o  19898  efopn  20005  cxpeq  20097  logreclem  20116  affineequiv  20123  quad2  20135  dcubic  20142  mcubic  20143  quart  20157  atandm2  20173  rlimcnp2  20261  amgm  20285  wilthlem2  20307  mumullem2  20418  sqff1o  20420  dvdsflip  20422  dvdsflf1o  20427  lgseisenlem2  20589  lgsquadlem2  20594  isgrpo  20863  isgrp2d  20902  grpodiveq  20923  opidon  20989  nvsubadd  21213  hvsubaddi  21645  hire  21673  shmodsi  21968  omlsilem  21981  chcon1i  22044  chnlei  22064  pjoml3i  22165  cmbr2i  22175  chscllem2  22217  adjsym  22413  eigorthi  22417  dfadj2  22465  adjval2  22471  cnvadj  22472  dmadjrnb  22486  adjvalval  22517  cnlnadjeui  22657  cnlnssadj  22660  adjbdln  22663  pjimai  22756  pjin2i  22773  pjin3i  22774  stadd3i  22828  largei  22847  cvnbtwn3  22868  cvnbtwn4  22869  mddmd2  22889  superpos  22934  atnemeq0  22957  sumdmdii  22995  sumdmdlem  22998  addltmulALT  23026  dfimafnf  23041  addeq0  23043  ballotlemi1  23061  ballotlemsima  23074  difeq  23128  mptfnf  23226  feqmptdf  23228  funcnvmptOLD  23234  funcnvmpt  23235  curry2ima  23247  elicoelioo  23271  xrmulc1cn  23303  xrge0iifcnv  23315  xrge0iifhom  23319  iundisj2fi  23364  iundisj2f  23366  disjrdx  23370  esumpcvgval  23446  esumcvg  23454  issgon  23484  ind1a  23604  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem9  23730  eupath2lem2  23902  br6  24114  fprb  24129  br1steq  24130  br2ndeq  24131  dfon2lem5  24143  dfon2lem8  24146  soseq  24254  sltval2  24310  sltintdifex  24317  sltres  24318  nofulllem5  24360  brbigcup  24438  dfbigcup2  24439  ellimits  24450  elfuns  24454  snelsingles  24461  dfiota3  24462  imageval  24469  brapply  24477  brsuccf  24480  brfullfun  24486  dfrdg4  24488  tfrqfree  24489  altopthbg  24502  altopthc  24505  altopthd  24506  altopelaltxp  24510  colinearalglem2  24535  colinearalg  24538  ax5seglem4  24560  ax5seglem5  24561  axlowdimlem13  24582  axeuclidlem  24590  axeuclid  24591  axcontlem2  24593  axcontlem4  24595  brsegle  24731  outsideofrflx  24750  copsexgb  24966  elo  25041  surjsec2  25120  sssu  25141  imtr  25398  cnvtr  25616  dualded  25783  dualcat2  25784  cmpmon  25815  iepiclem  25823  isconc2  26007  lineval4a  26087  hpd  26169  elicc3  26228  nn0prpw  26239  opnregcld  26248  cldregopn  26249  ssref  26283  fneval  26287  topfneec  26291  fdc  26455  heibor1  26534  0rngo  26652  smprngopr  26677  isfldidl  26693  isfldidl2  26694  elrfirn  26770  isnacs2  26781  isnacs3  26785  fiphp3d  26902  wopprc  27123  islnm2  27176  kercvrlsm  27181  phisum  27518  fgraphopab  27529  fmul01lt1lem2  27715  wallispilem4  27817  wallispi2lem1  27820  funressnfv  27991  afvpcfv0  28009  dfafn5a  28022  afvelrnb  28025  afvelrnb0  28026  dfaimafn2  28028  s2f1o  28091  nbcusgra  28159  opelopab4  28317  eqsbc3rVD  28616  bnj1366  28862  bnj553  28930  bnj964  28975  lcvnbtwn3  29218  lcvexchlem1  29224  lsatnem0  29235  opcon1b  29388  omllaw2N  29434  cmtbr2N  29443  leatb  29482  cvlsupr2  29533  glbconxN  29567  islln3  29699  llnexatN  29710  islpln3  29722  lplnexatN  29752  islvol3  29765  dalem-cly  29860  isline4N  29966  2llnma3r  29977  poml4N  30142  4atex2  30266  4atex2-0bOLDN  30268  cdlemefrs29bpre0  30585  cdlemftr3  30754  cdlemb3  30795  cdlemg17h  30857  cdlemg17pq  30861  cdlemg19  30873  cdlemg21  30875  tendoex  31164  dva1dim  31174  diarnN  31319  dihglb2  31532  doch11  31563  dochsordN  31564  lcfrlem9  31740  hlhillcs  32151
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator