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

Theorem incom 3361
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ancom 437 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  B  /\  x  e.  A )
)
2 elin 3358 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3358 . . 3  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
41, 2, 33bitr4i 268 . 2  |-  ( x  e.  ( A  i^i  B )  <->  x  e.  ( B  i^i  A ) )
54eqriv 2280 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1623    e. wcel 1684    i^i cin 3151
This theorem is referenced by:  ineq2  3364  dfss1  3373  in12  3380  in32  3381  in13  3382  in31  3383  inss2  3390  sslin  3395  inss  3398  indif1  3413  indifcom  3414  indir  3417  symdif1  3433  dfrab2  3443  disjr  3496  ssdifin0  3535  difdifdir  3541  uneqdifeq  3542  iinrab2  3965  iunin1  3967  iinin1  3973  riinn0  3976  rintn0  3992  disjprg  4019  disjxun  4021  inex2  4156  ordtri3or  4424  orduniss2  4624  resiun1  4974  dmres  4976  rescom  4980  resima2  4988  xpssres  4989  resopab  4996  imadisj  5032  ndmima  5050  intirr  5061  djudisj  5104  imainrect  5119  dmresv  5132  resdmres  5164  fnresdisj  5354  fnimaeq0  5365  resasplit  5411  fresaun  5412  fresaunres2  5413  fresaunres1  5414  fvun2  5591  ressnop0  5703  fvsnun1  5715  fsnunfv  5720  fnsuppeq0  5733  fveqf1o  5806  offres  6092  curry1  6210  curry2  6213  fpar  6222  smores3  6370  oacomf1o  6563  difsnen  6944  domunsncan  6962  domunsn  7011  limensuci  7037  phplem2  7041  pssnn  7081  dif1enOLD  7090  dif1en  7091  domunfican  7129  marypha1lem  7186  dfsup2OLD  7196  dfsup3OLD  7197  epfrs  7413  zfregs2  7415  tskwe  7583  dif1card  7638  dfac8b  7658  ac10ct  7661  kmlem11  7786  kmlem12  7787  cdacomen  7807  onacda  7823  ackbij1lem14  7859  ackbij1lem16  7861  ackbij1lem18  7863  fin23lem26  7951  fin23lem19  7962  fin23lem30  7968  isf32lem4  7982  isf34lem7  8005  isf34lem6  8006  axdc3lem4  8079  brdom7disj  8156  brdom6disj  8157  fpwwe2lem13  8264  canthp1lem1  8274  grothprim  8456  fseq1p1m1  10857  hashgval  11340  hashun3  11366  hashfun  11389  hashbclem  11390  limsupgle  11951  prmreclem2  12964  setsid  13187  ressinbas  13204  wunress  13207  mreexexlem2d  13547  mreexexlem4d  13549  oppcinv  13678  cnvps  14321  lsmmod2  14985  lsmdisj3  14992  lsmdisjr  14993  lsmdisj2r  14994  lsmdisj3r  14995  lsmdisj2a  14996  lsmdisj2b  14997  lsmdisj3a  14998  lsmdisj3b  14999  subgdisj2  15001  pj2f  15007  pj1id  15008  frgpuplem  15081  dprd2da  15277  dmdprdsplit2lem  15280  dmdprdsplit2  15281  pgpfaclem1  15316  lmhmlsp  15806  ltbwe  16214  psrbag0  16235  pjpm  16608  indistopon  16738  fctop  16741  cctop  16743  elcls  16810  mretopd  16829  restin  16897  restsn  16901  restcld  16903  resstopn  16916  lecldbas  16949  nrmsep  17085  regsep2  17104  isreg2  17105  ordthaus  17112  cmpsublem  17126  cmpsub  17127  hauscmplem  17133  iuncon  17154  cldllycmp  17221  kgentopon  17233  llycmpkgen2  17245  1stckgen  17249  txkgen  17346  kqcldsat  17424  regr1lem2  17431  fbun  17535  fin1aufil  17627  fclsfnflim  17722  metreslem  17926  blcld  18051  ressxms  18071  ressms  18072  reconn  18333  metdseq0  18358  metnrmlem3  18365  unmbl  18895  volun  18902  volinun  18903  iundisj2  18906  icombl  18921  ioombl  18922  uniioombllem2  18938  uniioombllem4  18941  dyaddisjlem  18950  dyaddisj  18951  mbfconstlem  18984  mbfeqalem  18997  ismbf3d  19009  itg1addlem5  19055  itgsplitioo  19192  lhop  19363  tdeglem4  19446  vieta1lem2  19691  xrlimcnp  20263  chtdif  20396  ppidif  20401  ppi1  20402  cht1  20403  perfectlem2  20469  rplogsum  20676  ex-dif  20810  ococi  21984  orthin  22025  lediri  22116  pjoml2i  22164  pjoml4i  22166  cmcmlem  22170  cmbr3i  22179  cmm2i  22186  cm0  22188  fh1  22197  fh2  22198  cm2j  22199  qlaxr3i  22215  pjclem2  22776  stm1ri  22824  golem1  22851  dmdbr5  22888  mddmd2  22889  cvmdi  22904  mdsldmd1i  22911  csmdsymi  22914  mdexchi  22915  cvexchi  22949  atssma  22958  atomli  22962  atoml2i  22963  atordi  22964  atcvatlem  22965  chirredlem1  22970  chirredlem2  22971  chirredlem3  22972  atcvat4i  22977  atabsi  22981  mdsymlem1  22983  dmdbr6ati  23003  cdj3lem3  23018  ballotlemfp1  23050  ballotlemfmpn  23053  ballotlemfval0  23054  ballotlemgun  23083  difeq  23128  inin  23167  df1stres  23243  df2ndres  23244  iocinif  23274  difioo  23275  xrge00  23311  disjdifprg  23352  iundisj2fi  23364  iundisj2f  23366  lmxrge0  23375  esumpfinvallem  23442  measxun2  23538  measvuni  23542  measinb  23548  totprobd  23629  probmeasb  23633  cndprobnul  23640  bayesth  23642  subfacp1lem3  23713  subfacp1lem5  23715  pconcon  23762  cvmscld  23804  cvmsss2  23805  epsetlike  24194  pred0  24199  wfi  24207  frind  24243  wfrlem5  24260  frrlem5  24285  nofulllem5  24360  inpws2  25043  moec  25047  neiopne  25051  domrancur1b  25200  domrancur1c  25202  inposet  25278  ranncnt  25283  basexre  25522  cnfilca  25556  islimrs4  25582  bwt2  25592  hdrmp  25706  inttaror  25900  carinttar  25902  bsstrs  26146  nbssntrs  26147  bosser  26167  pdiveql  26168  cldbnd  26244  sstotbnd2  26498  bndss  26510  fninfp  26754  ralxpmap  26761  elrfi  26769  coeq0  26831  diophrw  26838  eldioph2lem1  26839  eldioph2lem2  26840  diophin  26852  diophren  26896  dnwech  27145  fnwe2lem2  27148  kelac1  27161  kelac2lem  27162  kelac2  27163  lmhmlnmsplit  27185  pwssplit1  27188  pwssplit4  27191  pwfi2f1o  27260  islindf4  27308  pmtrmvd  27398  proot1hash  27519  diftpsneq  28070  zfregs2VD  28617  l1cvat  29245  pmod2iN  30038  pmodN  30039  pmodl42N  30040  osumcllem3N  30147  osumcllem4N  30148  dihmeetlem19N  31515  dihmeetALTN  31517
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-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159
  Copyright terms: Public domain W3C validator