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

Theorem incom 3374
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 3371 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3371 . . 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 2293 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1632    e. wcel 1696    i^i cin 3164
This theorem is referenced by:  ineq2  3377  dfss1  3386  in12  3393  in32  3394  in13  3395  in31  3396  inss2  3403  sslin  3408  inss  3411  indif1  3426  indifcom  3427  indir  3430  symdif1  3446  dfrab2  3456  disjr  3509  ssdifin0  3548  difdifdir  3554  uneqdifeq  3555  diftpsn3  3772  iinrab2  3981  iunin1  3983  iinin1  3989  riinn0  3992  rintn0  4008  disjprg  4035  disjxun  4037  inex2  4172  ordtri3or  4440  orduniss2  4640  resiun1  4990  dmres  4992  rescom  4996  resima2  5004  xpssres  5005  resopab  5012  imadisj  5048  ndmima  5066  intirr  5077  djudisj  5120  imainrect  5135  dmresv  5148  resdmres  5180  fnresdisj  5370  fnimaeq0  5381  resasplit  5427  fresaun  5428  fresaunres2  5429  fresaunres1  5430  fvun2  5607  ressnop0  5719  fvsnun1  5731  fsnunfv  5736  fnsuppeq0  5749  fveqf1o  5822  offres  6108  curry1  6226  curry2  6229  fpar  6238  smores3  6386  oacomf1o  6579  difsnen  6960  domunsncan  6978  domunsn  7027  limensuci  7053  phplem2  7057  pssnn  7097  dif1enOLD  7106  dif1en  7107  domunfican  7145  marypha1lem  7202  dfsup2OLD  7212  dfsup3OLD  7213  epfrs  7429  zfregs2  7431  tskwe  7599  dif1card  7654  dfac8b  7674  ac10ct  7677  kmlem11  7802  kmlem12  7803  cdacomen  7823  onacda  7839  ackbij1lem14  7875  ackbij1lem16  7877  ackbij1lem18  7879  fin23lem26  7967  fin23lem19  7978  fin23lem30  7984  isf32lem4  7998  isf34lem7  8021  isf34lem6  8022  axdc3lem4  8095  brdom7disj  8172  brdom6disj  8173  fpwwe2lem13  8280  canthp1lem1  8290  grothprim  8472  fseq1p1m1  10873  hashgval  11356  hashun3  11382  hashfun  11405  hashbclem  11406  limsupgle  11967  prmreclem2  12980  setsid  13203  ressinbas  13220  wunress  13223  mreexexlem2d  13563  mreexexlem4d  13565  oppcinv  13694  cnvps  14337  lsmmod2  15001  lsmdisj3  15008  lsmdisjr  15009  lsmdisj2r  15010  lsmdisj3r  15011  lsmdisj2a  15012  lsmdisj2b  15013  lsmdisj3a  15014  lsmdisj3b  15015  subgdisj2  15017  pj2f  15023  pj1id  15024  frgpuplem  15097  dprd2da  15293  dmdprdsplit2lem  15296  dmdprdsplit2  15297  pgpfaclem1  15332  lmhmlsp  15822  ltbwe  16230  psrbag0  16251  pjpm  16624  indistopon  16754  fctop  16757  cctop  16759  elcls  16826  mretopd  16845  restin  16913  restsn  16917  restcld  16919  resstopn  16932  lecldbas  16965  nrmsep  17101  regsep2  17120  isreg2  17121  ordthaus  17128  cmpsublem  17142  cmpsub  17143  hauscmplem  17149  iuncon  17170  cldllycmp  17237  kgentopon  17249  llycmpkgen2  17261  1stckgen  17265  txkgen  17362  kqcldsat  17440  regr1lem2  17447  fbun  17551  fin1aufil  17643  fclsfnflim  17738  metreslem  17942  blcld  18067  ressxms  18087  ressms  18088  reconn  18349  metdseq0  18374  metnrmlem3  18381  unmbl  18911  volun  18918  volinun  18919  iundisj2  18922  icombl  18937  ioombl  18938  uniioombllem2  18954  uniioombllem4  18957  dyaddisjlem  18966  dyaddisj  18967  mbfconstlem  19000  mbfeqalem  19013  ismbf3d  19025  itg1addlem5  19071  itgsplitioo  19208  lhop  19379  tdeglem4  19462  vieta1lem2  19707  xrlimcnp  20279  chtdif  20412  ppidif  20417  ppi1  20418  cht1  20419  perfectlem2  20485  rplogsum  20692  ex-dif  20826  ococi  22000  orthin  22041  lediri  22132  pjoml2i  22180  pjoml4i  22182  cmcmlem  22186  cmbr3i  22195  cmm2i  22202  cm0  22204  fh1  22213  fh2  22214  cm2j  22215  qlaxr3i  22231  pjclem2  22792  stm1ri  22840  golem1  22867  dmdbr5  22904  mddmd2  22905  cvmdi  22920  mdsldmd1i  22927  csmdsymi  22930  mdexchi  22931  cvexchi  22965  atssma  22974  atomli  22978  atoml2i  22979  atordi  22980  atcvatlem  22981  chirredlem1  22986  chirredlem2  22987  chirredlem3  22988  atcvat4i  22993  atabsi  22997  mdsymlem1  22999  dmdbr6ati  23019  cdj3lem3  23034  ballotlemfp1  23066  ballotlemfmpn  23069  ballotlemfval0  23070  ballotlemgun  23099  difeq  23144  inin  23183  df1stres  23258  df2ndres  23259  iocinif  23289  difioo  23290  xrge00  23326  disjdifprg  23367  iundisj2fi  23379  iundisj2f  23381  lmxrge0  23390  esumpfinvallem  23457  measxun2  23553  measvuni  23557  measinb  23563  totprobd  23644  probmeasb  23648  cndprobnul  23655  bayesth  23657  subfacp1lem3  23728  subfacp1lem5  23730  pconcon  23777  cvmscld  23819  cvmsss2  23820  epsetlike  24265  pred0  24270  wfi  24278  frind  24314  wfrlem5  24331  frrlem5  24356  nofulllem5  24431  inpws2  25146  moec  25150  neiopne  25154  domrancur1b  25303  domrancur1c  25305  inposet  25381  ranncnt  25386  basexre  25625  cnfilca  25659  islimrs4  25685  bwt2  25695  hdrmp  25809  inttaror  26003  carinttar  26005  bsstrs  26249  nbssntrs  26250  bosser  26270  pdiveql  26271  cldbnd  26347  sstotbnd2  26601  bndss  26613  fninfp  26857  ralxpmap  26864  elrfi  26872  coeq0  26934  diophrw  26941  eldioph2lem1  26942  eldioph2lem2  26943  diophin  26955  diophren  26999  dnwech  27248  fnwe2lem2  27251  kelac1  27264  kelac2lem  27265  kelac2  27266  lmhmlnmsplit  27288  pwssplit1  27291  pwssplit4  27294  pwfi2f1o  27363  islindf4  27411  pmtrmvd  27501  proot1hash  27622  zfregs2VD  28933  l1cvat  29867  pmod2iN  30660  pmodN  30661  pmodl42N  30662  osumcllem3N  30769  osumcllem4N  30770  dihmeetlem19N  32137  dihmeetALTN  32139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172
  Copyright terms: Public domain W3C validator