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

Theorem incom 3269
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 3266 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3266 . . 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 2250 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 3077
This theorem is referenced by:  ineq2  3272  dfss1  3281  in12  3287  in32  3288  in13  3289  in31  3290  inss2  3297  sslin  3302  inss  3305  indif1  3320  indifcom  3321  indir  3324  symdif1  3340  dfrab2  3350  disjr  3403  ssdifin0  3441  difdifdir  3447  uneqdifeq  3448  iinrab2  3863  iunin1  3865  iinin1  3871  riinn0  3874  rintn0  3890  disjprg  3916  disjxun  3918  inex2  4053  ordtri3or  4317  orduniss2  4515  resiun1  4881  dmres  4883  rescom  4887  resima2  4895  xpssres  4896  resopab  4903  imadisj  4939  ndmima  4957  intirr  4968  djudisj  5011  imainrect  5026  dmresv  5038  resdmres  5070  fnresdisj  5211  fnimaeq0  5222  resasplit  5268  fresaun  5269  fresaunres2  5270  fresaunres1  5271  fvun2  5443  ressnop0  5555  fvsnun1  5567  fsnunfv  5572  fnsuppeq0  5585  fveqf1o  5658  offres  5944  curry1  6062  curry2  6065  fpar  6074  smores3  6256  oacomf1o  6449  difsnen  6829  domunsncan  6847  domunsn  6896  limensuci  6922  phplem2  6926  pssnn  6966  dif1enOLD  6975  dif1en  6976  domunfican  7014  marypha1lem  7070  dfsup2OLD  7080  dfsup3OLD  7081  epfrs  7297  zfregs2  7299  tskwe  7467  dif1card  7522  dfac8b  7542  ac10ct  7545  kmlem11  7670  kmlem12  7671  cdacomen  7691  onacda  7707  ackbij1lem14  7743  ackbij1lem16  7745  ackbij1lem18  7747  fin23lem26  7835  fin23lem19  7846  fin23lem30  7852  isf32lem4  7866  isf34lem7  7889  isf34lem6  7890  axdc3lem4  7963  brdom7disj  8040  brdom6disj  8041  fpwwe2lem13  8144  canthp1lem1  8154  grothprim  8336  fseq1p1m1  10735  hashgval  11218  hashfun  11266  hashbclem  11267  limsupgle  11828  prmreclem2  12838  setsid  13061  ressinbas  13078  wunress  13081  oppcinv  13522  cnvps  14156  lsmmod2  14820  lsmdisj3  14827  lsmdisjr  14828  lsmdisj2r  14829  lsmdisj3r  14830  lsmdisj2a  14831  lsmdisj2b  14832  lsmdisj3a  14833  lsmdisj3b  14834  subgdisj2  14836  pj2f  14842  pj1id  14843  frgpuplem  14916  dprd2da  15112  dmdprdsplit2lem  15115  dmdprdsplit2  15116  pgpfaclem1  15151  lmhmlsp  15641  ltbwe  16046  psrbag0  16067  pjpm  16440  indistopon  16570  fctop  16573  cctop  16575  elcls  16642  mretopd  16661  restin  16729  restsn  16733  restcld  16735  resstopn  16748  lecldbas  16781  nrmsep  16917  regsep2  16936  isreg2  16937  ordthaus  16944  cmpsublem  16958  cmpsub  16959  hauscmplem  16965  iuncon  16986  cldllycmp  17053  kgentopon  17065  llycmpkgen2  17077  1stckgen  17081  txkgen  17178  kqcldsat  17256  regr1lem2  17263  fbun  17367  fin1aufil  17459  fclsfnflim  17554  metreslem  17758  blcld  17883  ressxms  17903  ressms  17904  reconn  18165  metdseq0  18190  metnrmlem3  18197  unmbl  18727  volun  18734  volinun  18735  iundisj2  18738  icombl  18753  ioombl  18754  uniioombllem2  18770  uniioombllem4  18773  dyaddisjlem  18782  dyaddisj  18783  mbfconstlem  18816  mbfeqalem  18829  ismbf3d  18841  itg1addlem5  18887  itgsplitioo  19024  lhop  19195  tdeglem4  19278  vieta1lem2  19523  xrlimcnp  20095  chtdif  20228  ppidif  20233  ppi1  20234  cht1  20235  perfectlem2  20301  rplogsum  20508  ex-dif  20623  ococi  21814  orthin  21855  lediri  21946  pjoml2i  22012  pjoml4i  22014  cmcmlem  22018  cmbr3i  22027  cmm2i  22034  cm0  22036  fh1  22045  fh2  22046  cm2j  22047  qlaxr3i  22063  pjclem2  22606  stm1ri  22654  golem1  22681  dmdbr5  22718  mddmd2  22719  cvmdi  22734  mdsldmd1i  22741  csmdsymi  22744  mdexchi  22745  cvexchi  22779  atssma  22788  atomli  22792  atoml2i  22793  atordi  22794  atcvatlem  22795  chirredlem1  22800  chirredlem2  22801  chirredlem3  22802  atcvat4i  22807  atabsi  22811  mdsymlem1  22813  dmdbr6ati  22833  cdj3lem3  22848  subfacp1lem3  22884  subfacp1lem5  22886  pconcon  22933  cvmscld  22975  cvmsss2  22976  epsetlike  23362  pred0  23367  wfi  23375  frind  23411  wfrlem5  23428  frrlem5  23453  inpws2  24208  moec  24212  neiopne  24216  repfuntw  24326  domrancur1b  24366  domrancur1c  24368  inposet  24444  ranncnt  24449  basexre  24688  cnfilca  24722  islimrs4  24748  bwt2  24758  hdrmp  24872  inttaror  25066  carinttar  25068  bsstrs  25312  nbssntrs  25313  bosser  25333  pdiveql  25334  cldbnd  25410  sstotbnd2  25664  bndss  25676  fninfp  25920  ralxpmap  25927  elrfi  25935  coeq0  25997  diophrw  26004  eldioph2lem1  26005  eldioph2lem2  26006  diophin  26018  diophren  26062  dnwech  26311  fnwe2lem2  26314  kelac1  26327  kelac2lem  26328  kelac2  26329  lmhmlnmsplit  26351  pwssplit1  26354  pwssplit4  26357  pwfi2f1o  26426  islindf4  26474  pmtrmvd  26564  proot1hash  26685  zfregs2VD  27307  l1cvat  27934  pmod2iN  28727  pmodN  28728  pmodl42N  28729  osumcllem3N  28836  osumcllem4N  28837  dihmeetlem19N  30204  dihmeetALTN  30206
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085
  Copyright terms: Public domain W3C validator