Theorem incom 3538

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

Syntax hints:   /\ wa 369   = wceq 1369   e. wcel 1756   i^i cin 3322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330

This theorem is referenced by:  ineq2  3541  dfss1  3550  in12  3556  in32  3557  in13  3558  in31  3559  inss2  3566  sslin  3571  inss  3574  indif1  3589  indifcom  3590  indir  3593  symdif1  3610  dfrab2  3621  disjr  3715  ssdifin0  3755  difdifdir  3761  uneqdifeq  3762  diftpsn3  4007  iinrab2  4228  iunin1  4230  iinin1  4236  riinn0  4240  rintn0  4256  disjprg  4283  disjxun  4285  inex2  4429  ordtri3or  4746  resiun1  5124  dmres  5126  rescom  5130  resima2  5138  xpssres  5139  resindm  5146  resdmdfsn  5147  resopab  5148  imadisj  5183  ndmima  5200  intirr  5211  djudisj  5260  imainrect  5274  dmresv  5291  resdmres  5324  fnresdisj  5516  fnimaeq0  5527  resasplit  5576  fresaun  5577  fresaunres2  5578  fresaunres1  5579  fvun2  5758  ressnop0  5884  fninfp  5900  fvsnun1  5908  fsnunfv  5913  fnsuppeq0OLD  5934  fveqf1o  5995  orduniss2  6439  offres  6567  curry1  6659  curry2  6662  fpar  6671  fnsuppeq0  6712  smores3  6806  oacomf1o  6996  ralxpmap  7254  difsnen  7385  domunsncan  7403  domunsn  7453  limensuci  7479  phplem2  7483  pssnn  7523  dif1enOLD  7536  dif1en  7537  domunfican  7576  marypha1lem  7675  dfsup2OLD  7685  dfsup3OLD  7686  epfrs  7943  zfregs2  7945  tskwe  8112  dif1card  8169  dfac8b  8193  ac10ct  8196  kmlem11  8321  kmlem12  8322  cdacomen  8342  onacda  8358  ackbij1lem14  8394  ackbij1lem16  8396  ackbij1lem18  8398  fin23lem26  8486  fin23lem19  8497  fin23lem30  8503  isf32lem4  8517  isf34lem7  8540  isf34lem6  8541  axdc3lem4  8614  brdom7disj  8690  brdom6disj  8691  fpwwe2lem13  8801  canthp1lem1  8811  grothprim  8993  fzpreddisj  11496  fzdifsuc  11508  fseq1p1m1  11526  hashgval  12098  hashun3  12139  hashfun  12191  hashbclem  12197  limsupgle  12947  prmreclem2  13970  setsid  14207  ressinbas  14226  wunress  14229  mreexexlem2d  14575  mreexexlem4d  14577  oppcinv  14706  cnvps  15374  pmtrmvd  15953  lsmmod2  16164  lsmdisj3  16171  lsmdisjr  16172  lsmdisj2r  16173  lsmdisj3r  16174  lsmdisj2a  16175  lsmdisj2b  16176  lsmdisj3a  16177  lsmdisj3b  16178  subgdisj2  16180  pj2f  16186  pj1id  16187  frgpuplem  16260  dprd2da  16531  dmdprdsplit2lem  16534  dmdprdsplit2  16535  pgpfaclem1  16572  lmhmlsp  17110  pwssplit1  17120  ltbwe  17534  psrbag0  17556  psgndiflemB  18010  pjpm  18113  islindf4  18247  indistopon  18585  fctop  18588  cctop  18590  elcls  18657  mretopd  18676  restin  18750  restsn  18754  restcld  18756  neitr  18764  resstopn  18770  lecldbas  18803  nrmsep  18941  regsep2  18960  isreg2  18961  ordthaus  18968  cmpsublem  18982  cmpsub  18983  hauscmplem  18989  bwth  18993  bwthOLD  18994  iuncon  19012  cldllycmp  19079  kgentopon  19091  llycmpkgen2  19103  1stckgen  19107  txkgen  19205  kqcldsat  19286  regr1lem2  19293  fbun  19393  fin1aufil  19485  fclsfnflim  19580  ustexsym  19770  restutopopn  19793  ustuqtop5  19800  ressuss  19818  metreslem  19917  blcld  20060  ressxms  20080  ressms  20081  restmetu  20142  reconn  20385  metdseq0  20410  metnrmlem3  20417  unmbl  20999  volun  21006  volinun  21007  iundisj2  21010  icombl  21025  ioombl  21026  uniioombllem2  21043  uniioombllem4  21046  dyaddisjlem  21055  dyaddisj  21056  mbfconstlem  21087  mbfeqalem  21100  ismbf3d  21112  itg1addlem5  21158  itgsplitioo  21295  lhop  21468  tdeglem4  21509  vieta1lem2  21757  xrlimcnp  22342  chtdif  22476  ppidif  22481  ppi1  22482  cht1  22483  perfectlem2  22549  rplogsum  22756  perpcom  23080  cusgrasizeindslem2  23350  ex-dif  23598  ococi  24776  orthin  24817  lediri  24908  pjoml2i  24956  pjoml4i  24958  cmcmlem  24962  cmbr3i  24971  cmm2i  24978  cm0  24980  fh1  24989  fh2  24990  cm2j  24991  qlaxr3i  25007  pjclem2  25568  stm1ri  25616  golem1  25643  dmdbr5  25680  mddmd2  25681  cvmdi  25696  mdsldmd1i  25703  csmdsymi  25706  mdexchi  25707  cvexchi  25741  atssma  25750  atomli  25754  atoml2i  25755  atordi  25756  atcvatlem  25757  chirredlem1  25762  chirredlem2  25763  chirredlem3  25764  atcvat4i  25769  atabsi  25773  mdsymlem1  25775  dmdbr6ati  25795  cdj3lem3  25810  inin  25864  difeq  25867  disjdifprg  25887  iundisj2f  25900  disjunsn  25904  imadifxp  25907  fnresin  25915  ofpreima2  25953  df1stres  25967  df2ndres  25968  iocinif  26039  difioo  26040  iundisj2fi  26049  xrge00  26115  xrge0slmod  26281  ordtconlem1  26323  lmxrge0  26351  esumpfinvallem  26492  measxun2  26593  measvuni  26597  measunl  26599  measinb  26604  eulerpartlemt  26723  eulerpartgbij  26724  probmeasb  26782  cndprobnul  26789  bayesth  26791  ballotlemfp1  26843  ballotlemfval0  26847  ballotlemgun  26876  signstres  26945  subfacp1lem3  27039  subfacp1lem5  27041  pconcon  27089  cvmscld  27131  cvmsss2  27132  dfpred3  27604  epsetlike  27624  pred0  27629  wfi  27637  frind  27673  wfrlem5  27697  frrlem5  27741  nofulllem5  27816  fin2so  28387  ptrest  28396  mblfinlem2  28400  mblfinlem3  28401  mblfinlem4  28402  ismblfin  28403  cnambfre  28411  asindmre  28450  dvasin  28451  dvreasin  28453  dvreacos  28454  cldbnd  28492  sstotbnd2  28644  bndss  28656  elrfi  29001  coeq0  29061  diophrw  29068  eldioph2lem1  29069  eldioph2lem2  29070  diophin  29082  diophren  29123  dnwech  29372  fnwe2lem2  29375  kelac1  29387  kelac2lem  29388  kelac2  29389  lmhmlnmsplit  29411  pwssplit4  29413  pwfi2f1o  29422  proot1hash  29539  f0rn0  30112  zfregs2VD  31506  iunconlem2  31600  bj-2upln1upl  32417  bj-diagval  32425  l1cvat  32593  pmod2iN  33386  pmodN  33387  pmodl42N  33388  osumcllem3N  33495  osumcllem4N  33496  dihmeetlem19N  34863  dihmeetALTN  34865