Theorem incom 3605

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 448	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3601	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3601	. . 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 2378	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 367   = wceq 1399   e. wcel 1826   i^i cin 3388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396

This theorem is referenced by:  ineq2  3608  dfss1  3617  in12  3623  in32  3624  in13  3625  in31  3626  inss2  3633  sslin  3638  inss  3641  indif1  3667  indifcom  3668  indir  3671  dfsymdif3  3688  symdif1OLD  3689  dfrab2  3699  disjr  3784  ssdifin0  3825  difdifdir  3831  uneqdifeq  3832  diftpsn3  4082  iinrab2  4306  iunin1  4308  iinin1  4314  riinn0  4318  rintn0  4337  disjprg  4363  disjxun  4365  inex2  4507  ordtri3or  4824  resiun1  5204  dmres  5206  rescom  5210  resima2  5219  xpssres  5220  resindm  5230  resdmdfsn  5231  resopab  5232  imadisj  5268  ndmimaOLD  5286  intirr  5298  djudisj  5344  imainrect  5358  dmresv  5374  resdmres  5406  coeq0  5424  fnresdisj  5599  fnimaeq0  5610  resasplit  5663  fresaun  5664  fresaunres2  5665  fresaunres1  5666  f0rn0  5678  fvun2  5846  fveqressseq  5929  ressnop0  5980  fninfp  6000  fvsnun1  6008  fsnunfv  6013  fveqf1o  6106  orduniss2  6567  offres  6694  curry1  6791  curry2  6794  fpar  6803  fnsuppeq0  6846  smores3  6942  oacomf1o  7132  ralxpmap  7387  difsnen  7518  domunsncan  7536  domunsn  7586  limensuci  7612  phplem2  7616  pssnn  7654  dif1en  7668  domunfican  7708  marypha1lem  7808  dfsup2OLD  7818  epfrs  8075  zfregs2  8077  tskwe  8244  dif1card  8301  dfac8b  8325  ac10ct  8328  kmlem11  8453  kmlem12  8454  cdacomen  8474  onacda  8490  ackbij1lem14  8526  ackbij1lem16  8528  ackbij1lem18  8530  fin23lem26  8618  fin23lem19  8629  fin23lem30  8635  isf32lem4  8649  isf34lem7  8672  isf34lem6  8673  axdc3lem4  8746  brdom7disj  8822  brdom6disj  8823  fpwwe2lem13  8931  canthp1lem1  8941  grothprim  9123  fzpreddisj  11651  fzdifsuc  11661  fseq1p1m1  11674  hashgval  12310  hashun3  12355  hashfun  12399  hashbclem  12405  xpcoidgend  12813  cotr2  12815  limsupgle  13302  prmreclem2  14437  setsid  14677  ressinbas  14697  wunress  14701  mreexexlem2d  15052  mreexexlem4d  15054  oppcinv  15186  cnvps  15959  pmtrmvd  16598  lsmmod2  16811  lsmdisj3  16818  lsmdisjr  16819  lsmdisj2r  16820  lsmdisj3r  16821  lsmdisj2a  16822  lsmdisj2b  16823  lsmdisj3a  16824  lsmdisj3b  16825  subgdisj2  16827  pj2f  16833  pj1id  16834  frgpuplem  16907  gsummptfzsplitl  17069  dprd2da  17204  dmdprdsplit2lem  17207  dmdprdsplit2  17208  pgpfaclem1  17245  lmhmlsp  17808  pwssplit1  17818  ltbwe  18250  psrbag0  18272  psgndiflemB  18727  pjpm  18830  islindf4  18958  indistopon  19587  fctop  19590  cctop  19592  elcls  19660  mretopd  19679  restin  19753  restsn  19757  restcld  19759  neitr  19767  resstopn  19773  lecldbas  19806  nrmsep  19944  regsep2  19963  isreg2  19964  ordthaus  19971  cmpsublem  19985  cmpsub  19986  hauscmplem  19992  bwth  19996  iuncon  20014  cldllycmp  20081  kgentopon  20124  llycmpkgen2  20136  1stckgen  20140  txkgen  20238  kqcldsat  20319  regr1lem2  20326  fbun  20426  fin1aufil  20518  fclsfnflim  20613  ustexsym  20803  restutopopn  20826  ustuqtop5  20833  ressuss  20851  metreslem  20950  blcld  21093  ressxms  21113  ressms  21114  restmetu  21175  reconn  21418  metdseq0  21443  metnrmlem3  21450  unmbl  22033  volun  22040  volinun  22041  iundisj2  22044  icombl  22059  ioombl  22060  uniioombllem2  22077  uniioombllem4  22080  dyaddisjlem  22089  dyaddisj  22090  mbfconstlem  22121  mbfeqalem  22134  ismbf3d  22146  itg1addlem5  22192  itgsplitioo  22329  lhop  22502  tdeglem4  22543  vieta1lem2  22792  xrlimcnp  23415  chtdif  23549  ppidif  23554  ppi1  23555  cht1  23556  perfectlem2  23622  rplogsum  23829  perpcom  24210  cusgrasizeindslem2  24595  ex-dif  25265  ococi  26440  orthin  26481  lediri  26572  pjoml2i  26620  pjoml4i  26622  cmcmlem  26626  cmbr3i  26635  cmm2i  26642  cm0  26644  fh1  26653  fh2  26654  cm2j  26655  qlaxr3i  26671  pjclem2  27231  stm1ri  27279  golem1  27306  dmdbr5  27343  mddmd2  27344  cvmdi  27359  mdsldmd1i  27366  csmdsymi  27369  mdexchi  27370  cvexchi  27404  atssma  27413  atomli  27417  atoml2i  27418  atordi  27419  atcvatlem  27420  chirredlem1  27425  chirredlem2  27426  chirredlem3  27427  atcvat4i  27432  atabsi  27436  mdsymlem1  27438  dmdbr6ati  27458  cdj3lem3  27473  inin  27531  difeq  27534  disjdifprg  27565  iundisj2f  27579  disjunsn  27583  imadifxp  27591  fnresin  27608  ofpreima2  27654  df1stres  27669  df2ndres  27670  padct  27695  iocinif  27745  difioo  27746  iundisj2fi  27755  xrge00  27827  xrge0slmod  27988  ordtconlem1  28060  lmxrge0  28088  esumrnmpt2  28216  esumpfinvallem  28222  measxun2  28337  measvuni  28341  measunl  28343  measinb  28348  carsgclctunlem1  28444  carsgclctunlem2  28446  eulerpartlemt  28493  eulerpartgbij  28494  probmeasb  28552  cndprobnul  28559  bayesth  28561  ballotlemfp1  28613  ballotlemfval0  28617  ballotlemgun  28646  signstres  28715  subfacp1lem3  28815  subfacp1lem5  28817  pconcon  28865  cvmscld  28907  cvmsss2  28908  mrsubvrs  29071  mthmpps  29131  dfpred3  29419  epsetlike  29439  pred0  29444  wfi  29452  frind  29488  wfrlem5  29512  frrlem5  29556  nofulllem5  29631  fin2so  30205  ptrest  30213  mblfinlem2  30217  mblfinlem3  30218  mblfinlem4  30219  ismblfin  30220  cnambfre  30228  asindmre  30268  dvasin  30269  dvreasin  30271  dvreacos  30272  cldbnd  30310  sstotbnd2  30436  bndss  30448  elrfi  30792  diophrw  30857  eldioph2lem1  30858  eldioph2lem2  30859  diophin  30871  diophren  30912  dnwech  31160  fnwe2lem2  31163  kelac1  31175  kelac2lem  31176  kelac2  31177  lmhmlnmsplit  31199  pwssplit4  31201  pwfi2f1o  31210  pwfi2f1oOLD  31211  proot1hash  31328  hashnzfz  31393  iccdifioo  31721  sumnnodd  31802  cncfuni  31855  fouriersw  32180  perfectALTVlem2  32544  rnghmsscmap2  32981  rnghmsubcsetclem1  32983  rnghmsubcsetc  32985  rngccat  32986  rngcid  32987  rngchomrnghmresALTV  33004  rngcifuestrc  33005  funcrngcsetc  33006  rhmsscmap2  33027  rhmsubcsetclem1  33029  rhmsubcsetc  33031  ringccat  33032  ringcid  33033  rhmsscrnghm  33034  rhmsubcrngclem1  33035  rhmsubcrngc  33037  rngcresringcat  33038  funcringcsetc  33043  rngcrescrhm  33093  rhmsubclem3  33096  rhmsubc  33098  rngcrescrhmALTV  33112  rhmsubcALTVlem3  33115  rhmsubcALTVlem4  33116  zfregs2VD  33987  iunconlem2  34082  bj-inrab3  34844  bj-2upln1upl  34930  bj-diagval  34953  l1cvat  35193  pmod2iN  35986  pmodN  35987  pmodl42N  35988  osumcllem3N  36095  osumcllem4N  36096  dihmeetlem19N  37465  dihmeetALTN  37467  rp-fakeuninass  38171  conrel1d  38192  dfrcl2  38211  iunrelexp0  38242