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

Theorem incom 3303
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 3300 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3300 . . 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 2253 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 3093
This theorem is referenced by:  ineq2  3306  dfss1  3315  in12  3322  in32  3323  in13  3324  in31  3325  inss2  3332  sslin  3337  inss  3340  indif1  3355  indifcom  3356  indir  3359  symdif1  3375  dfrab2  3385  disjr  3438  ssdifin0  3477  difdifdir  3483  uneqdifeq  3484  iinrab2  3906  iunin1  3908  iinin1  3914  riinn0  3917  rintn0  3933  disjprg  3959  disjxun  3961  inex2  4096  ordtri3or  4361  orduniss2  4561  resiun1  4927  dmres  4929  rescom  4933  resima2  4941  xpssres  4942  resopab  4949  imadisj  4985  ndmima  5003  intirr  5014  djudisj  5057  imainrect  5072  dmresv  5084  resdmres  5116  fnresdisj  5257  fnimaeq0  5268  resasplit  5314  fresaun  5315  fresaunres2  5316  fresaunres1  5317  fvun2  5490  ressnop0  5602  fvsnun1  5614  fsnunfv  5619  fnsuppeq0  5632  fveqf1o  5705  offres  5991  curry1  6109  curry2  6112  fpar  6121  smores3  6303  oacomf1o  6496  difsnen  6877  domunsncan  6895  domunsn  6944  limensuci  6970  phplem2  6974  pssnn  7014  dif1enOLD  7023  dif1en  7024  domunfican  7062  marypha1lem  7119  dfsup2OLD  7129  dfsup3OLD  7130  epfrs  7346  zfregs2  7348  tskwe  7516  dif1card  7571  dfac8b  7591  ac10ct  7594  kmlem11  7719  kmlem12  7720  cdacomen  7740  onacda  7756  ackbij1lem14  7792  ackbij1lem16  7794  ackbij1lem18  7796  fin23lem26  7884  fin23lem19  7895  fin23lem30  7901  isf32lem4  7915  isf34lem7  7938  isf34lem6  7939  axdc3lem4  8012  brdom7disj  8089  brdom6disj  8090  fpwwe2lem13  8197  canthp1lem1  8207  grothprim  8389  fseq1p1m1  10788  hashgval  11271  hashfun  11319  hashbclem  11320  limsupgle  11881  prmreclem2  12891  setsid  13114  ressinbas  13131  wunress  13134  mreexexlem2d  13474  mreexexlem4d  13476  oppcinv  13605  cnvps  14248  lsmmod2  14912  lsmdisj3  14919  lsmdisjr  14920  lsmdisj2r  14921  lsmdisj3r  14922  lsmdisj2a  14923  lsmdisj2b  14924  lsmdisj3a  14925  lsmdisj3b  14926  subgdisj2  14928  pj2f  14934  pj1id  14935  frgpuplem  15008  dprd2da  15204  dmdprdsplit2lem  15207  dmdprdsplit2  15208  pgpfaclem1  15243  lmhmlsp  15733  ltbwe  16141  psrbag0  16162  pjpm  16535  indistopon  16665  fctop  16668  cctop  16670  elcls  16737  mretopd  16756  restin  16824  restsn  16828  restcld  16830  resstopn  16843  lecldbas  16876  nrmsep  17012  regsep2  17031  isreg2  17032  ordthaus  17039  cmpsublem  17053  cmpsub  17054  hauscmplem  17060  iuncon  17081  cldllycmp  17148  kgentopon  17160  llycmpkgen2  17172  1stckgen  17176  txkgen  17273  kqcldsat  17351  regr1lem2  17358  fbun  17462  fin1aufil  17554  fclsfnflim  17649  metreslem  17853  blcld  17978  ressxms  17998  ressms  17999  reconn  18260  metdseq0  18285  metnrmlem3  18292  unmbl  18822  volun  18829  volinun  18830  iundisj2  18833  icombl  18848  ioombl  18849  uniioombllem2  18865  uniioombllem4  18868  dyaddisjlem  18877  dyaddisj  18878  mbfconstlem  18911  mbfeqalem  18924  ismbf3d  18936  itg1addlem5  18982  itgsplitioo  19119  lhop  19290  tdeglem4  19373  vieta1lem2  19618  xrlimcnp  20190  chtdif  20323  ppidif  20328  ppi1  20329  cht1  20330  perfectlem2  20396  rplogsum  20603  ex-dif  20718  ococi  21909  orthin  21950  lediri  22041  pjoml2i  22107  pjoml4i  22109  cmcmlem  22113  cmbr3i  22122  cmm2i  22129  cm0  22131  fh1  22140  fh2  22141  cm2j  22142  qlaxr3i  22158  pjclem2  22701  stm1ri  22749  golem1  22776  dmdbr5  22813  mddmd2  22814  cvmdi  22829  mdsldmd1i  22836  csmdsymi  22839  mdexchi  22840  cvexchi  22874  atssma  22883  atomli  22887  atoml2i  22888  atordi  22889  atcvatlem  22890  chirredlem1  22895  chirredlem2  22896  chirredlem3  22897  atcvat4i  22902  atabsi  22906  mdsymlem1  22908  dmdbr6ati  22928  cdj3lem3  22943  ballotlemfp1  22976  ballotlemfmpn  22979  ballotlemfval0  22980  ballotlemgun  23009  subfacp1lem3  23050  subfacp1lem5  23052  pconcon  23099  cvmscld  23141  cvmsss2  23142  epsetlike  23528  pred0  23533  wfi  23541  frind  23577  wfrlem5  23594  frrlem5  23619  inpws2  24374  moec  24378  neiopne  24382  repfuntw  24492  domrancur1b  24532  domrancur1c  24534  inposet  24610  ranncnt  24615  basexre  24854  cnfilca  24888  islimrs4  24914  bwt2  24924  hdrmp  25038  inttaror  25232  carinttar  25234  bsstrs  25478  nbssntrs  25479  bosser  25499  pdiveql  25500  cldbnd  25576  sstotbnd2  25830  bndss  25842  fninfp  26086  ralxpmap  26093  elrfi  26101  coeq0  26163  diophrw  26170  eldioph2lem1  26171  eldioph2lem2  26172  diophin  26184  diophren  26228  dnwech  26477  fnwe2lem2  26480  kelac1  26493  kelac2lem  26494  kelac2  26495  lmhmlnmsplit  26517  pwssplit1  26520  pwssplit4  26523  pwfi2f1o  26592  islindf4  26640  pmtrmvd  26730  proot1hash  26851  zfregs2VD  27630  l1cvat  28375  pmod2iN  29168  pmodN  29169  pmodl42N  29170  osumcllem3N  29277  osumcllem4N  29278  dihmeetlem19N  30645  dihmeetALTN  30647
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101
  Copyright terms: Public domain W3C validator