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

Theorem incom 3362
Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
incom  |-  ( A  i^i  B )  =  ( B  i^i  A
)

Proof of Theorem incom
StepHypRef Expression
1 ancom 439 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  B  /\  x  e.  A )
)
2 elin 3359 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3359 . . 3  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
41, 2, 33bitr4i 270 . 2  |-  ( x  e.  ( A  i^i  B )  <->  x  e.  ( B  i^i  A ) )
54eqriv 2281 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1628    e. wcel 1688    i^i cin 3152
This theorem is referenced by:  ineq2  3365  dfss1  3374  in12  3381  in32  3382  in13  3383  in31  3384  inss2  3391  sslin  3396  inss  3399  indif1  3414  indifcom  3415  indir  3418  symdif1  3434  dfrab2  3444  disjr  3497  ssdifin0  3536  difdifdir  3542  uneqdifeq  3543  iinrab2  3966  iunin1  3968  iinin1  3974  riinn0  3977  rintn0  3993  disjprg  4020  disjxun  4022  inex2  4157  ordtri3or  4423  orduniss2  4623  resiun1  4973  dmres  4975  rescom  4979  resima2  4987  xpssres  4988  resopab  4995  imadisj  5031  ndmima  5049  intirr  5060  djudisj  5103  imainrect  5118  dmresv  5130  resdmres  5162  fnresdisj  5319  fnimaeq0  5330  resasplit  5376  fresaun  5377  fresaunres2  5378  fresaunres1  5379  fvun2  5552  ressnop0  5664  fvsnun1  5676  fsnunfv  5681  fnsuppeq0  5694  fveqf1o  5767  offres  6053  curry1  6171  curry2  6174  fpar  6183  smores3  6365  oacomf1o  6558  difsnen  6939  domunsncan  6957  domunsn  7006  limensuci  7032  phplem2  7036  pssnn  7076  dif1enOLD  7085  dif1en  7086  domunfican  7124  marypha1lem  7181  dfsup2OLD  7191  dfsup3OLD  7192  epfrs  7408  zfregs2  7410  tskwe  7578  dif1card  7633  dfac8b  7653  ac10ct  7656  kmlem11  7781  kmlem12  7782  cdacomen  7802  onacda  7818  ackbij1lem14  7854  ackbij1lem16  7856  ackbij1lem18  7858  fin23lem26  7946  fin23lem19  7957  fin23lem30  7963  isf32lem4  7977  isf34lem7  8000  isf34lem6  8001  axdc3lem4  8074  brdom7disj  8151  brdom6disj  8152  fpwwe2lem13  8259  canthp1lem1  8269  grothprim  8451  fseq1p1m1  10851  hashgval  11334  hashun3  11360  hashfun  11383  hashbclem  11384  limsupgle  11945  prmreclem2  12958  setsid  13181  ressinbas  13198  wunress  13201  mreexexlem2d  13541  mreexexlem4d  13543  oppcinv  13672  cnvps  14315  lsmmod2  14979  lsmdisj3  14986  lsmdisjr  14987  lsmdisj2r  14988  lsmdisj3r  14989  lsmdisj2a  14990  lsmdisj2b  14991  lsmdisj3a  14992  lsmdisj3b  14993  subgdisj2  14995  pj2f  15001  pj1id  15002  frgpuplem  15075  dprd2da  15271  dmdprdsplit2lem  15274  dmdprdsplit2  15275  pgpfaclem1  15310  lmhmlsp  15800  ltbwe  16208  psrbag0  16229  pjpm  16602  indistopon  16732  fctop  16735  cctop  16737  elcls  16804  mretopd  16823  restin  16891  restsn  16895  restcld  16897  resstopn  16910  lecldbas  16943  nrmsep  17079  regsep2  17098  isreg2  17099  ordthaus  17106  cmpsublem  17120  cmpsub  17121  hauscmplem  17127  iuncon  17148  cldllycmp  17215  kgentopon  17227  llycmpkgen2  17239  1stckgen  17243  txkgen  17340  kqcldsat  17418  regr1lem2  17425  fbun  17529  fin1aufil  17621  fclsfnflim  17716  metreslem  17920  blcld  18045  ressxms  18065  ressms  18066  reconn  18327  metdseq0  18352  metnrmlem3  18359  unmbl  18889  volun  18896  volinun  18897  iundisj2  18900  icombl  18915  ioombl  18916  uniioombllem2  18932  uniioombllem4  18935  dyaddisjlem  18944  dyaddisj  18945  mbfconstlem  18978  mbfeqalem  18991  ismbf3d  19003  itg1addlem5  19049  itgsplitioo  19186  lhop  19357  tdeglem4  19440  vieta1lem2  19685  xrlimcnp  20257  chtdif  20390  ppidif  20395  ppi1  20396  cht1  20397  perfectlem2  20463  rplogsum  20670  ex-dif  20785  ococi  21976  orthin  22017  lediri  22108  pjoml2i  22156  pjoml4i  22158  cmcmlem  22162  cmbr3i  22171  cmm2i  22178  cm0  22180  fh1  22189  fh2  22190  cm2j  22191  qlaxr3i  22207  pjclem2  22768  stm1ri  22816  golem1  22843  dmdbr5  22880  mddmd2  22881  cvmdi  22896  mdsldmd1i  22903  csmdsymi  22906  mdexchi  22907  cvexchi  22941  atssma  22950  atomli  22954  atoml2i  22955  atordi  22956  atcvatlem  22957  chirredlem1  22962  chirredlem2  22963  chirredlem3  22964  atcvat4i  22969  atabsi  22973  mdsymlem1  22975  dmdbr6ati  22995  cdj3lem3  23010  ballotlemfp1  23043  ballotlemfmpn  23046  ballotlemfval0  23047  ballotlemgun  23076  subfacp1lem3  23117  subfacp1lem5  23119  pconcon  23166  cvmscld  23208  cvmsss2  23209  epsetlike  23595  pred0  23600  wfi  23608  frind  23644  wfrlem5  23661  frrlem5  23686  inpws2  24441  moec  24445  neiopne  24449  repfuntw  24559  domrancur1b  24599  domrancur1c  24601  inposet  24677  ranncnt  24682  basexre  24921  cnfilca  24955  islimrs4  24981  bwt2  24991  hdrmp  25105  inttaror  25299  carinttar  25301  bsstrs  25545  nbssntrs  25546  bosser  25566  pdiveql  25567  cldbnd  25643  sstotbnd2  25897  bndss  25909  fninfp  26153  ralxpmap  26160  elrfi  26168  coeq0  26230  diophrw  26237  eldioph2lem1  26238  eldioph2lem2  26239  diophin  26251  diophren  26295  dnwech  26544  fnwe2lem2  26547  kelac1  26560  kelac2lem  26561  kelac2  26562  lmhmlnmsplit  26584  pwssplit1  26587  pwssplit4  26590  pwfi2f1o  26659  islindf4  26707  pmtrmvd  26797  proot1hash  26918  zfregs2VD  27885  l1cvat  28512  pmod2iN  29305  pmodN  29306  pmodl42N  29307  osumcllem3N  29414  osumcllem4N  29415  dihmeetlem19N  30782  dihmeetALTN  30784
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160
  Copyright terms: Public domain W3C validator