Theorem incom 3676

Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-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.

Step	Hyp	Ref	Expression
1		ancom 450	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3672	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3672	. . 3 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
4	1, 2, 3	3bitr4i 277	. 2 |- ( x e. ( A i^i B ) <-> x e. ( B i^i A ) )
5	4	eqriv 2439	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 369   = wceq 1383   e. wcel 1804   i^i cin 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468

This theorem is referenced by:  ineq2  3679  dfss1  3688  in12  3694  in32  3695  in13  3696  in31  3697  inss2  3704  sslin  3709  inss  3712  indif1  3727  indifcom  3728  indir  3731  symdif1  3748  dfrab2  3759  disjr  3854  ssdifin0  3895  difdifdir  3901  uneqdifeq  3902  diftpsn3  4153  iinrab2  4378  iunin1  4380  iinin1  4386  riinn0  4390  rintn0  4406  disjprg  4433  disjxun  4435  inex2  4579  ordtri3or  4900  resiun1  5282  dmres  5284  rescom  5288  resima2  5297  xpssres  5298  resindm  5308  resdmdfsn  5309  resopab  5310  imadisj  5346  ndmima  5363  intirr  5375  djudisj  5424  imainrect  5438  dmresv  5455  resdmres  5488  coeq0  5506  fnresdisj  5681  fnimaeq0  5692  resasplit  5745  fresaun  5746  fresaunres2  5747  fresaunres1  5748  f0rn0  5760  fvun2  5930  fveqressseq  6012  ressnop0  6063  fninfp  6083  fvsnun1  6091  fsnunfv  6096  fnsuppeq0OLD  6117  fveqf1o  6190  orduniss2  6653  offres  6780  curry1  6877  curry2  6880  fpar  6889  fnsuppeq0  6930  smores3  7026  oacomf1o  7216  ralxpmap  7470  difsnen  7601  domunsncan  7619  domunsn  7669  limensuci  7695  phplem2  7699  pssnn  7740  dif1enOLD  7754  dif1en  7755  domunfican  7795  marypha1lem  7895  dfsup2OLD  7905  dfsup3OLD  7906  epfrs  8165  zfregs2  8167  tskwe  8334  dif1card  8391  dfac8b  8415  ac10ct  8418  kmlem11  8543  kmlem12  8544  cdacomen  8564  onacda  8580  ackbij1lem14  8616  ackbij1lem16  8618  ackbij1lem18  8620  fin23lem26  8708  fin23lem19  8719  fin23lem30  8725  isf32lem4  8739  isf34lem7  8762  isf34lem6  8763  axdc3lem4  8836  brdom7disj  8912  brdom6disj  8913  fpwwe2lem13  9023  canthp1lem1  9033  grothprim  9215  fzpreddisj  11738  fzdifsuc  11748  fseq1p1m1  11761  hashgval  12387  hashun3  12431  hashfun  12474  hashbclem  12480  limsupgle  13279  prmreclem2  14312  setsid  14550  ressinbas  14570  wunress  14573  mreexexlem2d  14919  mreexexlem4d  14921  oppcinv  15047  cnvps  15716  pmtrmvd  16355  lsmmod2  16568  lsmdisj3  16575  lsmdisjr  16576  lsmdisj2r  16577  lsmdisj3r  16578  lsmdisj2a  16579  lsmdisj2b  16580  lsmdisj3a  16581  lsmdisj3b  16582  subgdisj2  16584  pj2f  16590  pj1id  16591  frgpuplem  16664  gsummptfzsplitl  16827  dprd2da  16965  dmdprdsplit2lem  16968  dmdprdsplit2  16969  pgpfaclem1  17006  lmhmlsp  17569  pwssplit1  17579  ltbwe  18011  psrbag0  18033  psgndiflemB  18509  pjpm  18612  islindf4  18746  indistopon  19375  fctop  19378  cctop  19380  elcls  19447  mretopd  19466  restin  19540  restsn  19544  restcld  19546  neitr  19554  resstopn  19560  lecldbas  19593  nrmsep  19731  regsep2  19750  isreg2  19751  ordthaus  19758  cmpsublem  19772  cmpsub  19773  hauscmplem  19779  bwth  19783  bwthOLD  19784  iuncon  19802  cldllycmp  19869  kgentopon  19912  llycmpkgen2  19924  1stckgen  19928  txkgen  20026  kqcldsat  20107  regr1lem2  20114  fbun  20214  fin1aufil  20306  fclsfnflim  20401  ustexsym  20591  restutopopn  20614  ustuqtop5  20621  ressuss  20639  metreslem  20738  blcld  20881  ressxms  20901  ressms  20902  restmetu  20963  reconn  21206  metdseq0  21231  metnrmlem3  21238  unmbl  21821  volun  21828  volinun  21829  iundisj2  21832  icombl  21847  ioombl  21848  uniioombllem2  21865  uniioombllem4  21868  dyaddisjlem  21877  dyaddisj  21878  mbfconstlem  21909  mbfeqalem  21922  ismbf3d  21934  itg1addlem5  21980  itgsplitioo  22117  lhop  22290  tdeglem4  22331  vieta1lem2  22579  xrlimcnp  23170  chtdif  23304  ppidif  23309  ppi1  23310  cht1  23311  perfectlem2  23377  rplogsum  23584  perpcom  23962  cusgrasizeindslem2  24346  ex-dif  25016  ococi  26195  orthin  26236  lediri  26327  pjoml2i  26375  pjoml4i  26377  cmcmlem  26381  cmbr3i  26390  cmm2i  26397  cm0  26399  fh1  26408  fh2  26409  cm2j  26410  qlaxr3i  26426  pjclem2  26987  stm1ri  27035  golem1  27062  dmdbr5  27099  mddmd2  27100  cvmdi  27115  mdsldmd1i  27122  csmdsymi  27125  mdexchi  27126  cvexchi  27160  atssma  27169  atomli  27173  atoml2i  27174  atordi  27175  atcvatlem  27176  chirredlem1  27181  chirredlem2  27182  chirredlem3  27183  atcvat4i  27188  atabsi  27192  mdsymlem1  27194  dmdbr6ati  27214  cdj3lem3  27229  inin  27285  difeq  27288  disjdifprg  27308  iundisj2f  27321  disjunsn  27325  imadifxp  27330  fnresin  27342  ofpreima2  27380  df1stres  27394  df2ndres  27395  iocinif  27464  difioo  27465  iundisj2fi  27474  xrge00  27547  xrge0slmod  27707  ordtconlem1  27779  lmxrge0  27807  esumpfinvallem  27953  measxun2  28054  measvuni  28058  measunl  28060  measinb  28065  eulerpartlemt  28183  eulerpartgbij  28184  probmeasb  28242  cndprobnul  28249  bayesth  28251  ballotlemfp1  28303  ballotlemfval0  28307  ballotlemgun  28336  signstres  28405  subfacp1lem3  28499  subfacp1lem5  28501  pconcon  28549  cvmscld  28591  cvmsss2  28592  mrsubvrs  28755  mthmpps  28815  dfpred3  29229  epsetlike  29249  pred0  29254  wfi  29262  frind  29298  wfrlem5  29322  frrlem5  29366  nofulllem5  29441  fin2so  30015  ptrest  30023  mblfinlem2  30027  mblfinlem3  30028  mblfinlem4  30029  ismblfin  30030  cnambfre  30038  asindmre  30077  dvasin  30078  dvreasin  30080  dvreacos  30081  cldbnd  30119  sstotbnd2  30245  bndss  30257  elrfi  30601  diophrw  30667  eldioph2lem1  30668  eldioph2lem2  30669  diophin  30681  diophren  30722  dnwech  30969  fnwe2lem2  30972  kelac1  30984  kelac2lem  30985  kelac2  30986  lmhmlnmsplit  31008  pwssplit4  31010  pwfi2f1o  31019  proot1hash  31136  hashnzfz  31201  iccdifioo  31491  sumnnodd  31544  cncfuni  31596  fouriersw  31903  rnghmsscmap2  32521  rnghmsubcsetclem1  32523  rnghmsubcsetc  32525  rngccat  32526  rngcid  32527  rngchomrnghmresOLD  32544  rngcifuestrc  32545  funcrngcsetc  32546  rhmsscmap2  32564  rhmsubcsetclem1  32566  rhmsubcsetc  32568  ringccat  32569  ringcid  32570  rhmsscrnghm  32571  rhmsubcrngclem1  32572  rhmsubcrngc  32574  rngcresringcat  32575  funcringcsetc  32580  rngcrescrhm  32626  rhmsubclem3  32629  rhmsubc  32631  rngcrescrhmOLD  32645  rhmsubcOLDlem3  32648  rhmsubcOLDlem4  32649  zfregs2VD  33374  iunconlem2  33468  bj-2upln1upl  34330  bj-diagval  34345  l1cvat  34520  pmod2iN  35313  pmodN  35314  pmodl42N  35315  osumcllem3N  35422  osumcllem4N  35423  dihmeetlem19N  36792  dihmeetALTN  36794  rp-fakeuninass  37444  conrel1d  37464  xpcoidgend  37467  cotr2  37480