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

Theorem eqcom 2360
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 1566 . 2  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  <->  A. x ( x  e.  B  <->  x  e.  A ) )
3 dfcleq 2352 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
4 dfcleq 2352 . 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 1540    = wceq 1642    e. wcel 1710
This theorem is referenced by:  eqcoms  2361  eqcomi  2362  eqcomd  2363  eqeq2  2367  eqtr2  2376  eqtr3  2377  abeq1  2464  pm13.181  2594  necom  2602  gencbvex  2906  reu7  3036  eqsbc3r  3124  dfss  3243  sspsstri  3354  dfss5  3450  disj4  3579  ssnelpss  3593  preqr1  3867  invdisj  4093  disjprg  4100  disjxun  4102  dtruALT  4288  dtruALT2  4300  opthg2  4329  copsexg  4334  copsex4g  4337  opcom  4342  opeqsn  4344  opeqpr  4345  opthwiener  4350  ordtri2  4509  suc11  4578  on0eqel  4592  snsn0non  4593  reusv3  4624  onmindif2  4685  opthprc  4818  elxp3  4821  opeliunxp  4822  relop  4916  dmopab3  4973  rncoeq  5030  intirr  5143  somin1  5161  xpcan  5194  xpcan2  5195  dfrel4v  5207  dmsnn0  5220  iota1  5315  sniota  5328  fresaunres1  5497  dffn5  5651  fvelrnb  5653  dfimafn2  5655  funimass4  5656  fnsnfv  5665  dmfco  5676  fndmdif  5712  fneqeql  5716  rexrn  5750  ralrn  5751  dffo4  5759  fconstfv  5820  rexima  5843  ralima  5844  fvclss  5846  dff13  5870  f1eqcocnv  5892  f1oiso  5935  oprabid  5969  eloprabga  6021  ovelimab  6085  dfoprab3  6263  brtpos2  6327  tpossym  6353  opiota  6377  eusvobj2  6424  f1ocnvfv3  6427  rdglim2  6532  tz7.48lem  6540  oaf1o  6648  omopthi  6742  erth2  6792  brecop  6839  erovlem  6842  ecopovsym  6848  eceqoveq  6851  xpcomco  7040  omxpenlem  7051  mapen  7113  nneneq  7132  unxpdomlem3  7157  unfilem1  7211  wemapso2lem  7355  suc11reg  7410  inf3lem2  7420  inf3lem6  7424  mapfien  7489  infenaleph  7808  isinfcard  7809  dfac5  7845  kmlem15  7880  cfeq0  7972  cfsuc  7973  ssfin4  8026  fin23lem25  8040  fin23lem22  8043  fin23lem40  8067  fin1a2lem5  8120  axcclem  8173  brdom7disj  8246  brdom6disj  8247  inar1  8487  psslinpr  8745  ltexprlem4  8753  ltsrpr  8789  mulgt0sr  8817  elreal  8843  ltresr  8852  leloe  8998  addsubeq4  9156  subcan2  9162  negcon1  9189  negcon2  9190  wloglei  9395  divmul2  9518  conjmul  9567  rereccl  9568  creur  9830  creui  9831  nndiv  9876  arch  10054  nn0sub  10106  elnn0z  10128  elznn0  10130  zq  10414  xrleloe  10570  dflt2  10574  ngtmnft  10588  icoshftf1o  10851  iccf1o  10870  fzen  10903  fzneuz  10955  mod0  11070  modirr  11101  nn0ennn  11133  hashsdom  11456  hashbclem  11486  hashfacen  11488  hashf1lem1  11489  cjreb  11704  leabs  11880  incexc2  12394  rpnnen2  12601  dvdsval2  12631  odd2np1  12684  oddm1even  12685  divalglem4  12692  divalglem8  12696  divalgb  12700  divalgmod  12702  hashdvds  12940  vdwlem12  13136  setcinv  14021  yonedainv  14154  latnle  14290  grpid  14616  grpinvcnv  14635  grplmulf1o  14641  grpsubeq0  14651  grpsubadd  14652  grplactcnv  14663  isnsg4  14759  conjghm  14812  conjnmzb  14816  gacan  14858  gapm  14859  cntzrec  14908  oppgcntz  14936  odmulgeq  14969  dfod2  14976  sylow3lem3  15039  sylow3lem6  15042  lssnle  15082  lsmhash  15113  efgredlemb  15154  efgrelexlemb  15158  dprd2d2  15378  ablfac1eulem  15406  pgpfac1lem2  15409  pgpfac1lem4  15412  dvdsrval  15526  dvdsr02  15537  lvecinv  15965  rspsn  16105  psrbagconf1o  16219  mplmonmul  16307  opsrtoslem1  16324  prmirredlem  16552  zndvds  16609  znleval  16614  istps2OLD  16765  cmpfi  17241  qtopeu  17513  hmeoimaf1o  17567  txhmeo  17600  fbasrn  17681  rnelfmlem  17749  hauspwpwf1  17784  alexsubALTlem4  17846  divstgpopn  17904  divstgphaus  17907  isngp3  18222  isngp4  18235  metnrmlem1a  18465  icopnfcnv  18544  iccpnfcnv  18546  ivthle  18920  ivthle2  18921  iundisj2  19010  dyadmbl  19059  mbfinf  19124  i1fmulclem  19161  itg1mulc  19163  mvth  19443  dvivth  19461  lhop2  19466  ply1divmo  19625  dvdsq1p  19650  reeff1o  19930  coseq1  19997  recosf1o  20004  resinf1o  20005  efopn  20116  cxpeq  20208  logreclem  20227  affineequiv  20234  quad2  20246  dcubic  20253  mcubic  20254  quart  20268  atandm2  20284  rlimcnp2  20372  amgm  20396  wilthlem2  20419  mumullem2  20530  sqff1o  20532  dvdsflip  20534  dvdsflf1o  20539  lgseisenlem2  20701  lgsquadlem2  20706  isgrpo  20975  isgrp2d  21014  grpodiveq  21035  opidon  21101  nvsubadd  21327  hvsubaddi  21759  hire  21787  shmodsi  22082  omlsilem  22095  chcon1i  22158  chnlei  22178  pjoml3i  22279  cmbr2i  22289  chscllem2  22331  adjsym  22527  eigorthi  22531  dfadj2  22579  adjval2  22585  cnvadj  22586  dmadjrnb  22600  adjvalval  22631  cnlnadjeui  22771  cnlnssadj  22774  adjbdln  22777  pjimai  22870  pjin2i  22887  pjin3i  22888  stadd3i  22942  largei  22961  cvnbtwn3  22982  cvnbtwn4  22983  mddmd2  23003  superpos  23048  atnemeq0  23071  sumdmdii  23109  sumdmdlem  23112  addltmulALT  23140  difeq  23196  iundisj2f  23228  disjrdx  23229  dfimafnf  23247  mptfnf  23277  feqmptdf  23279  funcnvmptOLD  23285  funcnvmpt  23286  curry2ima  23301  addeq0  23319  elicoelioo  23343  iundisj2fi  23357  xrmulc1cn  23472  xrge0iifcnv  23475  xrge0iifhom  23479  fmucndlem  23585  ind1a  23684  esumfsup  23726  esumpcvgval  23734  esumcvg  23742  issgon  23772  ballotlemi1  24009  ballotlemsima  24022  subfacp1lem3  24117  subfacp1lem5  24119  erdszelem9  24134  eupath2lem2  24306  gammadmaddnn0  24646  gammadenomn0  24648  br6  24672  fprb  24687  br1steq  24688  br2ndeq  24689  dfon2lem5  24701  dfon2lem8  24704  soseq  24812  sltval2  24868  sltintdifex  24875  sltres  24876  nofulllem5  24918  brbigcup  24996  dfbigcup2  24997  ellimits  25008  elfuns  25012  snelsingles  25019  dfiota3  25020  imageval  25027  brapply  25035  brsuccf  25038  funpartlem  25039  brfullfun  25045  dfrdg4  25047  tfrqfree  25048  altopthbg  25061  altopthc  25064  altopthd  25065  altopelaltxp  25069  colinearalglem2  25094  colinearalg  25097  ax5seglem4  25119  ax5seglem5  25120  axlowdimlem13  25141  axeuclidlem  25149  axeuclid  25150  axcontlem2  25152  axcontlem4  25154  brsegle  25290  outsideofrflx  25309  itg2addnclem2  25493  itgaddnclem2  25499  elicc3  25552  nn0prpw  25563  opnregcld  25572  cldregopn  25573  ssref  25607  fneval  25611  topfneec  25615  fdc  25779  heibor1  25857  0rngo  25975  smprngopr  26000  isfldidl  26016  isfldidl2  26017  elrfirn  26093  isnacs2  26104  isnacs3  26108  fiphp3d  26225  wopprc  26446  islnm2  26499  kercvrlsm  26504  phisum  26841  fgraphopab  26852  fmul01lt1lem2  27038  wallispilem4  27140  wallispi2lem1  27143  funressnfv  27316  afvpcfv0  27334  dfafn5a  27348  afvelrnb  27351  afvelrnb0  27352  dfaimafn2  27354  rabrsn  27413  ftpg  27417  elrnrexdmb  27428  injresinj  27465  hashtpg  27471  hashgt12el2  27473  brfi1uzind  27497  4fvwrd4  27499  s2f1o  27502  nbgraop1  27591  nbgraf1olem1  27605  nbgraf1olem5  27609  nbcusgra  27626  fargshiftfo  27761  eupatrl  27763  frgrawopreg2  27884  opelopab4  28062  eqsbc3rVD  28378  bnj1366  28624  bnj553  28692  bnj964  28737  lcvnbtwn3  29287  lcvexchlem1  29293  lsatnem0  29304  opcon1b  29457  omllaw2N  29503  cmtbr2N  29512  leatb  29551  cvlsupr2  29602  glbconxN  29636  islln3  29768  llnexatN  29779  islpln3  29791  lplnexatN  29821  islvol3  29834  dalem-cly  29929  isline4N  30035  2llnma3r  30046  poml4N  30211  4atex2  30335  4atex2-0bOLDN  30337  cdlemefrs29bpre0  30654  cdlemftr3  30823  cdlemb3  30864  cdlemg17h  30926  cdlemg17pq  30930  cdlemg19  30942  cdlemg21  30944  tendoex  31233  dva1dim  31243  diarnN  31388  dihglb2  31601  doch11  31632  dochsordN  31633  lcfrlem9  31809  hlhillcs  32220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-cleq 2351
  Copyright terms: Public domain W3C validator