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

Theorem incom 3336
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 3333 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3333 . . 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 2255 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1619    e. wcel 1621    i^i cin 3126
This theorem is referenced by:  ineq2  3339  dfss1  3348  in12  3355  in32  3356  in13  3357  in31  3358  inss2  3365  sslin  3370  inss  3373  indif1  3388  indifcom  3389  indir  3392  symdif1  3408  dfrab2  3418  disjr  3471  ssdifin0  3510  difdifdir  3516  uneqdifeq  3517  iinrab2  3939  iunin1  3941  iinin1  3947  riinn0  3950  rintn0  3966  disjprg  3993  disjxun  3995  inex2  4130  ordtri3or  4396  orduniss2  4596  resiun1  4962  dmres  4964  rescom  4968  resima2  4976  xpssres  4977  resopab  4984  imadisj  5020  ndmima  5038  intirr  5049  djudisj  5092  imainrect  5107  dmresv  5119  resdmres  5151  fnresdisj  5292  fnimaeq0  5303  resasplit  5349  fresaun  5350  fresaunres2  5351  fresaunres1  5352  fvun2  5525  ressnop0  5637  fvsnun1  5649  fsnunfv  5654  fnsuppeq0  5667  fveqf1o  5740  offres  6026  curry1  6144  curry2  6147  fpar  6156  smores3  6338  oacomf1o  6531  difsnen  6912  domunsncan  6930  domunsn  6979  limensuci  7005  phplem2  7009  pssnn  7049  dif1enOLD  7058  dif1en  7059  domunfican  7097  marypha1lem  7154  dfsup2OLD  7164  dfsup3OLD  7165  epfrs  7381  zfregs2  7383  tskwe  7551  dif1card  7606  dfac8b  7626  ac10ct  7629  kmlem11  7754  kmlem12  7755  cdacomen  7775  onacda  7791  ackbij1lem14  7827  ackbij1lem16  7829  ackbij1lem18  7831  fin23lem26  7919  fin23lem19  7930  fin23lem30  7936  isf32lem4  7950  isf34lem7  7973  isf34lem6  7974  axdc3lem4  8047  brdom7disj  8124  brdom6disj  8125  fpwwe2lem13  8232  canthp1lem1  8242  grothprim  8424  fseq1p1m1  10823  hashgval  11306  hashfun  11354  hashbclem  11355  limsupgle  11916  prmreclem2  12926  setsid  13149  ressinbas  13166  wunress  13169  mreexexlem2d  13509  mreexexlem4d  13511  oppcinv  13640  cnvps  14283  lsmmod2  14947  lsmdisj3  14954  lsmdisjr  14955  lsmdisj2r  14956  lsmdisj3r  14957  lsmdisj2a  14958  lsmdisj2b  14959  lsmdisj3a  14960  lsmdisj3b  14961  subgdisj2  14963  pj2f  14969  pj1id  14970  frgpuplem  15043  dprd2da  15239  dmdprdsplit2lem  15242  dmdprdsplit2  15243  pgpfaclem1  15278  lmhmlsp  15768  ltbwe  16176  psrbag0  16197  pjpm  16570  indistopon  16700  fctop  16703  cctop  16705  elcls  16772  mretopd  16791  restin  16859  restsn  16863  restcld  16865  resstopn  16878  lecldbas  16911  nrmsep  17047  regsep2  17066  isreg2  17067  ordthaus  17074  cmpsublem  17088  cmpsub  17089  hauscmplem  17095  iuncon  17116  cldllycmp  17183  kgentopon  17195  llycmpkgen2  17207  1stckgen  17211  txkgen  17308  kqcldsat  17386  regr1lem2  17393  fbun  17497  fin1aufil  17589  fclsfnflim  17684  metreslem  17888  blcld  18013  ressxms  18033  ressms  18034  reconn  18295  metdseq0  18320  metnrmlem3  18327  unmbl  18857  volun  18864  volinun  18865  iundisj2  18868  icombl  18883  ioombl  18884  uniioombllem2  18900  uniioombllem4  18903  dyaddisjlem  18912  dyaddisj  18913  mbfconstlem  18946  mbfeqalem  18959  ismbf3d  18971  itg1addlem5  19017  itgsplitioo  19154  lhop  19325  tdeglem4  19408  vieta1lem2  19653  xrlimcnp  20225  chtdif  20358  ppidif  20363  ppi1  20364  cht1  20365  perfectlem2  20431  rplogsum  20638  ex-dif  20753  ococi  21944  orthin  21985  lediri  22076  pjoml2i  22124  pjoml4i  22126  cmcmlem  22130  cmbr3i  22139  cmm2i  22146  cm0  22148  fh1  22157  fh2  22158  cm2j  22159  qlaxr3i  22175  pjclem2  22736  stm1ri  22784  golem1  22811  dmdbr5  22848  mddmd2  22849  cvmdi  22864  mdsldmd1i  22871  csmdsymi  22874  mdexchi  22875  cvexchi  22909  atssma  22918  atomli  22922  atoml2i  22923  atordi  22924  atcvatlem  22925  chirredlem1  22930  chirredlem2  22931  chirredlem3  22932  atcvat4i  22937  atabsi  22941  mdsymlem1  22943  dmdbr6ati  22963  cdj3lem3  22978  ballotlemfp1  23011  ballotlemfmpn  23014  ballotlemfval0  23015  ballotlemgun  23044  subfacp1lem3  23085  subfacp1lem5  23087  pconcon  23134  cvmscld  23176  cvmsss2  23177  epsetlike  23563  pred0  23568  wfi  23576  frind  23612  wfrlem5  23629  frrlem5  23654  inpws2  24409  moec  24413  neiopne  24417  repfuntw  24527  domrancur1b  24567  domrancur1c  24569  inposet  24645  ranncnt  24650  basexre  24889  cnfilca  24923  islimrs4  24949  bwt2  24959  hdrmp  25073  inttaror  25267  carinttar  25269  bsstrs  25513  nbssntrs  25514  bosser  25534  pdiveql  25535  cldbnd  25611  sstotbnd2  25865  bndss  25877  fninfp  26121  ralxpmap  26128  elrfi  26136  coeq0  26198  diophrw  26205  eldioph2lem1  26206  eldioph2lem2  26207  diophin  26219  diophren  26263  dnwech  26512  fnwe2lem2  26515  kelac1  26528  kelac2lem  26529  kelac2  26530  lmhmlnmsplit  26552  pwssplit1  26555  pwssplit4  26558  pwfi2f1o  26627  islindf4  26675  pmtrmvd  26765  proot1hash  26886  zfregs2VD  27667  l1cvat  28412  pmod2iN  29205  pmodN  29206  pmodl42N  29207  osumcllem3N  29314  osumcllem4N  29315  dihmeetlem19N  30682  dihmeetALTN  30684
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134
  Copyright terms: Public domain W3C validator