Theorem incom 3650

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 3646	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3646	. . 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 2450	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 369   = wceq 1370   e. wcel 1758   i^i cin 3434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-in 3442

This theorem is referenced by:  ineq2  3653  dfss1  3662  in12  3668  in32  3669  in13  3670  in31  3671  inss2  3678  sslin  3683  inss  3686  indif1  3701  indifcom  3702  indir  3705  symdif1  3722  dfrab2  3733  disjr  3827  ssdifin0  3867  difdifdir  3873  uneqdifeq  3874  diftpsn3  4119  iinrab2  4340  iunin1  4342  iinin1  4348  riinn0  4352  rintn0  4368  disjprg  4395  disjxun  4397  inex2  4541  ordtri3or  4858  resiun1  5236  dmres  5238  rescom  5242  resima2  5250  xpssres  5251  resindm  5258  resdmdfsn  5259  resopab  5260  imadisj  5295  ndmima  5312  intirr  5323  djudisj  5372  imainrect  5386  dmresv  5403  resdmres  5436  fnresdisj  5628  fnimaeq0  5639  resasplit  5688  fresaun  5689  fresaunres2  5690  fresaunres1  5691  fvun2  5871  ressnop0  5997  fninfp  6013  fvsnun1  6021  fsnunfv  6026  fnsuppeq0OLD  6047  fveqf1o  6108  orduniss2  6553  offres  6681  curry1  6773  curry2  6776  fpar  6785  fnsuppeq0  6826  smores3  6923  oacomf1o  7113  ralxpmap  7371  difsnen  7502  domunsncan  7520  domunsn  7570  limensuci  7596  phplem2  7600  pssnn  7641  dif1enOLD  7654  dif1en  7655  domunfican  7694  marypha1lem  7793  dfsup2OLD  7803  dfsup3OLD  7804  epfrs  8061  zfregs2  8063  tskwe  8230  dif1card  8287  dfac8b  8311  ac10ct  8314  kmlem11  8439  kmlem12  8440  cdacomen  8460  onacda  8476  ackbij1lem14  8512  ackbij1lem16  8514  ackbij1lem18  8516  fin23lem26  8604  fin23lem19  8615  fin23lem30  8621  isf32lem4  8635  isf34lem7  8658  isf34lem6  8659  axdc3lem4  8732  brdom7disj  8808  brdom6disj  8809  fpwwe2lem13  8919  canthp1lem1  8929  grothprim  9111  fzpreddisj  11620  fzdifsuc  11632  fseq1p1m1  11650  hashgval  12222  hashun3  12264  hashfun  12316  hashbclem  12322  limsupgle  13072  prmreclem2  14095  setsid  14332  ressinbas  14352  wunress  14355  mreexexlem2d  14701  mreexexlem4d  14703  oppcinv  14832  cnvps  15500  pmtrmvd  16080  lsmmod2  16293  lsmdisj3  16300  lsmdisjr  16301  lsmdisj2r  16302  lsmdisj3r  16303  lsmdisj2a  16304  lsmdisj2b  16305  lsmdisj3a  16306  lsmdisj3b  16307  subgdisj2  16309  pj2f  16315  pj1id  16316  frgpuplem  16389  gsummptfzsplitl  16547  dprd2da  16662  dmdprdsplit2lem  16665  dmdprdsplit2  16666  pgpfaclem1  16703  lmhmlsp  17252  pwssplit1  17262  ltbwe  17677  psrbag0  17699  psgndiflemB  18154  pjpm  18257  islindf4  18391  indistopon  18736  fctop  18739  cctop  18741  elcls  18808  mretopd  18827  restin  18901  restsn  18905  restcld  18907  neitr  18915  resstopn  18921  lecldbas  18954  nrmsep  19092  regsep2  19111  isreg2  19112  ordthaus  19119  cmpsublem  19133  cmpsub  19134  hauscmplem  19140  bwth  19144  bwthOLD  19145  iuncon  19163  cldllycmp  19230  kgentopon  19242  llycmpkgen2  19254  1stckgen  19258  txkgen  19356  kqcldsat  19437  regr1lem2  19444  fbun  19544  fin1aufil  19636  fclsfnflim  19731  ustexsym  19921  restutopopn  19944  ustuqtop5  19951  ressuss  19969  metreslem  20068  blcld  20211  ressxms  20231  ressms  20232  restmetu  20293  reconn  20536  metdseq0  20561  metnrmlem3  20568  unmbl  21151  volun  21158  volinun  21159  iundisj2  21162  icombl  21177  ioombl  21178  uniioombllem2  21195  uniioombllem4  21198  dyaddisjlem  21207  dyaddisj  21208  mbfconstlem  21239  mbfeqalem  21252  ismbf3d  21264  itg1addlem5  21310  itgsplitioo  21447  lhop  21620  tdeglem4  21661  vieta1lem2  21909  xrlimcnp  22494  chtdif  22628  ppidif  22633  ppi1  22634  cht1  22635  perfectlem2  22701  rplogsum  22908  perpcom  23248  cusgrasizeindslem2  23533  ex-dif  23781  ococi  24959  orthin  25000  lediri  25091  pjoml2i  25139  pjoml4i  25141  cmcmlem  25145  cmbr3i  25154  cmm2i  25161  cm0  25163  fh1  25172  fh2  25173  cm2j  25174  qlaxr3i  25190  pjclem2  25751  stm1ri  25799  golem1  25826  dmdbr5  25863  mddmd2  25864  cvmdi  25879  mdsldmd1i  25886  csmdsymi  25889  mdexchi  25890  cvexchi  25924  atssma  25933  atomli  25937  atoml2i  25938  atordi  25939  atcvatlem  25940  chirredlem1  25945  chirredlem2  25946  chirredlem3  25947  atcvat4i  25952  atabsi  25956  mdsymlem1  25958  dmdbr6ati  25978  cdj3lem3  25993  inin  26047  difeq  26050  disjdifprg  26069  iundisj2f  26082  disjunsn  26086  imadifxp  26089  fnresin  26097  ofpreima2  26135  df1stres  26149  df2ndres  26150  iocinif  26215  difioo  26216  iundisj2fi  26225  xrge00  26291  xrge0slmod  26456  ordtconlem1  26498  lmxrge0  26526  esumpfinvallem  26667  measxun2  26768  measvuni  26772  measunl  26774  measinb  26779  eulerpartlemt  26897  eulerpartgbij  26898  probmeasb  26956  cndprobnul  26963  bayesth  26965  ballotlemfp1  27017  ballotlemfval0  27021  ballotlemgun  27050  signstres  27119  subfacp1lem3  27213  subfacp1lem5  27215  pconcon  27263  cvmscld  27305  cvmsss2  27306  dfpred3  27778  epsetlike  27798  pred0  27803  wfi  27811  frind  27847  wfrlem5  27871  frrlem5  27915  nofulllem5  27990  fin2so  28563  ptrest  28572  mblfinlem2  28576  mblfinlem3  28577  mblfinlem4  28578  ismblfin  28579  cnambfre  28587  asindmre  28626  dvasin  28627  dvreasin  28629  dvreacos  28630  cldbnd  28668  sstotbnd2  28820  bndss  28832  elrfi  29177  coeq0  29237  diophrw  29244  eldioph2lem1  29245  eldioph2lem2  29246  diophin  29258  diophren  29299  dnwech  29548  fnwe2lem2  29551  kelac1  29563  kelac2lem  29564  kelac2  29565  lmhmlnmsplit  29587  pwssplit4  29589  pwfi2f1o  29598  proot1hash  29715  f0rn0  30288  zfregs2VD  31894  iunconlem2  31988  bj-2upln1upl  32834  bj-diagval  32848  l1cvat  33023  pmod2iN  33816  pmodN  33817  pmodl42N  33818  osumcllem3N  33925  osumcllem4N  33926  dihmeetlem19N  35293  dihmeetALTN  35295