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

Theorem incom 3533
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 438 . . 3  |-  ( ( x  e.  A  /\  x  e.  B )  <->  ( x  e.  B  /\  x  e.  A )
)
2 elin 3530 . . 3  |-  ( x  e.  ( A  i^i  B )  <->  ( x  e.  A  /\  x  e.  B ) )
3 elin 3530 . . 3  |-  ( x  e.  ( B  i^i  A )  <->  ( x  e.  B  /\  x  e.  A ) )
41, 2, 33bitr4i 269 . 2  |-  ( x  e.  ( A  i^i  B )  <->  x  e.  ( B  i^i  A ) )
54eqriv 2433 1  |-  ( A  i^i  B )  =  ( B  i^i  A
)
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1652    e. wcel 1725    i^i cin 3319
This theorem is referenced by:  ineq2  3536  dfss1  3545  in12  3552  in32  3553  in13  3554  in31  3555  inss2  3562  sslin  3567  inss  3570  indif1  3585  indifcom  3586  indir  3589  symdif1  3606  dfrab2  3616  disjr  3669  ssdifin0  3709  difdifdir  3715  uneqdifeq  3716  diftpsn3  3937  iinrab2  4154  iunin1  4156  iinin1  4162  riinn0  4165  rintn0  4181  disjprg  4208  disjxun  4210  inex2  4345  ordtri3or  4613  orduniss2  4813  resiun1  5165  dmres  5167  rescom  5171  resima2  5179  xpssres  5180  resopab  5187  imadisj  5223  ndmima  5241  intirr  5252  djudisj  5297  imainrect  5312  dmresv  5329  resdmres  5361  fnresdisj  5555  fnimaeq0  5566  resasplit  5613  fresaun  5614  fresaunres2  5615  fresaunres1  5616  fvun2  5795  ressnop0  5913  fvsnun1  5928  fsnunfv  5933  fnsuppeq0  5953  fveqf1o  6029  offres  6319  curry1  6438  curry2  6441  fpar  6450  smores3  6615  oacomf1o  6808  difsnen  7190  domunsncan  7208  domunsn  7257  limensuci  7283  phplem2  7287  pssnn  7327  dif1enOLD  7340  dif1en  7341  domunfican  7379  marypha1lem  7438  dfsup2OLD  7448  dfsup3OLD  7449  epfrs  7667  zfregs2  7669  tskwe  7837  dif1card  7892  dfac8b  7912  ac10ct  7915  kmlem11  8040  kmlem12  8041  cdacomen  8061  onacda  8077  ackbij1lem14  8113  ackbij1lem16  8115  ackbij1lem18  8117  fin23lem26  8205  fin23lem19  8216  fin23lem30  8222  isf32lem4  8236  isf34lem7  8259  isf34lem6  8260  axdc3lem4  8333  brdom7disj  8409  brdom6disj  8410  fpwwe2lem13  8517  canthp1lem1  8527  grothprim  8709  fseq1p1m1  11122  hashgval  11621  hashun3  11658  hashfun  11700  hashbclem  11701  limsupgle  12271  prmreclem2  13285  setsid  13508  ressinbas  13525  wunress  13528  mreexexlem2d  13870  mreexexlem4d  13872  oppcinv  14001  cnvps  14644  lsmmod2  15308  lsmdisj3  15315  lsmdisjr  15316  lsmdisj2r  15317  lsmdisj3r  15318  lsmdisj2a  15319  lsmdisj2b  15320  lsmdisj3a  15321  lsmdisj3b  15322  subgdisj2  15324  pj2f  15330  pj1id  15331  frgpuplem  15404  dprd2da  15600  dmdprdsplit2lem  15603  dmdprdsplit2  15604  pgpfaclem1  15639  lmhmlsp  16125  ltbwe  16533  psrbag0  16554  pjpm  16935  indistopon  17065  fctop  17068  cctop  17070  elcls  17137  mretopd  17156  restin  17230  restsn  17234  restcld  17236  neitr  17244  resstopn  17250  lecldbas  17283  nrmsep  17421  regsep2  17440  isreg2  17441  ordthaus  17448  cmpsublem  17462  cmpsub  17463  hauscmplem  17469  bwth  17473  iuncon  17491  cldllycmp  17558  kgentopon  17570  llycmpkgen2  17582  1stckgen  17586  txkgen  17684  kqcldsat  17765  regr1lem2  17772  fbun  17872  fin1aufil  17964  fclsfnflim  18059  ustexsym  18245  restutopopn  18268  ustuqtop5  18275  ressuss  18293  metreslem  18392  blcld  18535  ressxms  18555  ressms  18556  restmetu  18617  reconn  18859  metdseq0  18884  metnrmlem3  18891  unmbl  19432  volun  19439  volinun  19440  iundisj2  19443  icombl  19458  ioombl  19459  uniioombllem2  19475  uniioombllem4  19478  dyaddisjlem  19487  dyaddisj  19488  mbfconstlem  19521  mbfeqalem  19534  ismbf3d  19546  itg1addlem5  19592  itgsplitioo  19729  lhop  19900  tdeglem4  19983  vieta1lem2  20228  xrlimcnp  20807  chtdif  20941  ppidif  20946  ppi1  20947  cht1  20948  perfectlem2  21014  rplogsum  21221  cusgrasizeindslem2  21483  ex-dif  21731  ococi  22907  orthin  22948  lediri  23039  pjoml2i  23087  pjoml4i  23089  cmcmlem  23093  cmbr3i  23102  cmm2i  23109  cm0  23111  fh1  23120  fh2  23121  cm2j  23122  qlaxr3i  23138  pjclem2  23699  stm1ri  23747  golem1  23774  dmdbr5  23811  mddmd2  23812  cvmdi  23827  mdsldmd1i  23834  csmdsymi  23837  mdexchi  23838  cvexchi  23872  atssma  23881  atomli  23885  atoml2i  23886  atordi  23887  atcvatlem  23888  chirredlem1  23893  chirredlem2  23894  chirredlem3  23895  atcvat4i  23900  atabsi  23904  mdsymlem1  23906  dmdbr6ati  23926  cdj3lem3  23941  inin  23996  difeq  23998  disjdifprg  24017  iundisj2f  24030  imadifxp  24038  df1stres  24091  df2ndres  24092  iocinif  24144  difioo  24145  iundisj2fi  24153  xrge00  24208  lmxrge0  24337  esumpfinvallem  24464  measxun2  24564  measvuni  24568  measunl  24570  measinb  24575  sibfof  24654  probmeasb  24688  cndprobnul  24695  bayesth  24697  ballotlemfp1  24749  ballotlemfval0  24753  ballotlemgun  24782  subfacp1lem3  24868  subfacp1lem5  24870  pconcon  24918  cvmscld  24960  cvmsss2  24961  dfpred3  25449  epsetlike  25469  pred0  25474  wfi  25482  frind  25518  wfrlem5  25542  frrlem5  25586  nofulllem5  25661  mblfinlem2  26244  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  cnambfre  26255  cldbnd  26329  sstotbnd2  26483  bndss  26495  fninfp  26735  ralxpmap  26742  elrfi  26748  coeq0  26810  diophrw  26817  eldioph2lem1  26818  eldioph2lem2  26819  diophin  26831  diophren  26874  dnwech  27123  fnwe2lem2  27126  kelac1  27138  kelac2lem  27139  kelac2  27140  lmhmlnmsplit  27162  pwssplit1  27165  pwssplit4  27168  pwfi2f1o  27237  islindf4  27285  pmtrmvd  27375  proot1hash  27496  zfregs2VD  28953  iunconlem2  29047  l1cvat  29853  pmod2iN  30646  pmodN  30647  pmodl42N  30648  osumcllem3N  30755  osumcllem4N  30756  dihmeetlem19N  32123  dihmeetALTN  32125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327
  Copyright terms: Public domain W3C validator