Theorem incom 3531

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.

Step	Hyp	Ref	Expression
1		ancom 448	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3527	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3527	. . 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 2430	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 369   = wceq 1362   e. wcel 1755   i^i cin 3315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323

This theorem is referenced by:  ineq2  3534  dfss1  3543  in12  3549  in32  3550  in13  3551  in31  3552  inss2  3559  sslin  3564  inss  3567  indif1  3582  indifcom  3583  indir  3586  symdif1  3603  dfrab2  3614  disjr  3708  ssdifin0  3748  difdifdir  3754  uneqdifeq  3755  diftpsn3  4000  iinrab2  4221  iunin1  4223  iinin1  4229  riinn0  4233  rintn0  4249  disjprg  4276  disjxun  4278  inex2  4422  ordtri3or  4738  resiun1  5117  dmres  5119  rescom  5123  resima2  5131  xpssres  5132  resindm  5139  resdmdfsn  5140  resopab  5141  imadisj  5176  ndmima  5193  intirr  5204  djudisj  5253  imainrect  5267  dmresv  5284  resdmres  5317  fnresdisj  5509  fnimaeq0  5520  resasplit  5569  fresaun  5570  fresaunres2  5571  fresaunres1  5572  fvun2  5751  ressnop0  5876  fninfp  5892  fvsnun1  5900  fsnunfv  5905  fnsuppeq0OLD  5926  fveqf1o  5987  orduniss2  6433  offres  6561  curry1  6653  curry2  6656  fpar  6665  fnsuppeq0  6706  smores3  6800  oacomf1o  6992  ralxpmap  7250  difsnen  7381  domunsncan  7399  domunsn  7449  limensuci  7475  phplem2  7479  pssnn  7519  dif1enOLD  7532  dif1en  7533  domunfican  7572  marypha1lem  7671  dfsup2OLD  7681  dfsup3OLD  7682  epfrs  7939  zfregs2  7941  tskwe  8108  dif1card  8165  dfac8b  8189  ac10ct  8192  kmlem11  8317  kmlem12  8318  cdacomen  8338  onacda  8354  ackbij1lem14  8390  ackbij1lem16  8392  ackbij1lem18  8394  fin23lem26  8482  fin23lem19  8493  fin23lem30  8499  isf32lem4  8513  isf34lem7  8536  isf34lem6  8537  axdc3lem4  8610  brdom7disj  8686  brdom6disj  8687  fpwwe2lem13  8797  canthp1lem1  8807  grothprim  8989  fseq1p1m1  11518  hashgval  12090  hashun3  12131  hashfun  12183  hashbclem  12189  limsupgle  12939  prmreclem2  13961  setsid  14198  ressinbas  14217  wunress  14220  mreexexlem2d  14566  mreexexlem4d  14568  oppcinv  14697  cnvps  15365  pmtrmvd  15942  lsmmod2  16153  lsmdisj3  16160  lsmdisjr  16161  lsmdisj2r  16162  lsmdisj3r  16163  lsmdisj2a  16164  lsmdisj2b  16165  lsmdisj3a  16166  lsmdisj3b  16167  subgdisj2  16169  pj2f  16175  pj1id  16176  frgpuplem  16249  dprd2da  16515  dmdprdsplit2lem  16518  dmdprdsplit2  16519  pgpfaclem1  16556  lmhmlsp  17052  pwssplit1  17062  ltbwe  17486  psrbag0  17508  psgndiflemB  17872  pjpm  17975  islindf4  18109  indistopon  18447  fctop  18450  cctop  18452  elcls  18519  mretopd  18538  restin  18612  restsn  18616  restcld  18618  neitr  18626  resstopn  18632  lecldbas  18665  nrmsep  18803  regsep2  18822  isreg2  18823  ordthaus  18830  cmpsublem  18844  cmpsub  18845  hauscmplem  18851  bwth  18855  bwthOLD  18856  iuncon  18874  cldllycmp  18941  kgentopon  18953  llycmpkgen2  18965  1stckgen  18969  txkgen  19067  kqcldsat  19148  regr1lem2  19155  fbun  19255  fin1aufil  19347  fclsfnflim  19442  ustexsym  19632  restutopopn  19655  ustuqtop5  19662  ressuss  19680  metreslem  19779  blcld  19922  ressxms  19942  ressms  19943  restmetu  20004  reconn  20247  metdseq0  20272  metnrmlem3  20279  unmbl  20861  volun  20868  volinun  20869  iundisj2  20872  icombl  20887  ioombl  20888  uniioombllem2  20905  uniioombllem4  20908  dyaddisjlem  20917  dyaddisj  20918  mbfconstlem  20949  mbfeqalem  20962  ismbf3d  20974  itg1addlem5  21020  itgsplitioo  21157  lhop  21330  tdeglem4  21414  vieta1lem2  21662  xrlimcnp  22247  chtdif  22381  ppidif  22386  ppi1  22387  cht1  22388  perfectlem2  22454  rplogsum  22661  cusgrasizeindslem2  23205  ex-dif  23453  ococi  24631  orthin  24672  lediri  24763  pjoml2i  24811  pjoml4i  24813  cmcmlem  24817  cmbr3i  24826  cmm2i  24833  cm0  24835  fh1  24844  fh2  24845  cm2j  24846  qlaxr3i  24862  pjclem2  25423  stm1ri  25471  golem1  25498  dmdbr5  25535  mddmd2  25536  cvmdi  25551  mdsldmd1i  25558  csmdsymi  25561  mdexchi  25562  cvexchi  25596  atssma  25605  atomli  25609  atoml2i  25610  atordi  25611  atcvatlem  25612  chirredlem1  25617  chirredlem2  25618  chirredlem3  25619  atcvat4i  25624  atabsi  25628  mdsymlem1  25630  dmdbr6ati  25650  cdj3lem3  25665  inin  25720  difeq  25723  disjdifprg  25743  iundisj2f  25756  disjunsn  25760  imadifxp  25763  fnresin  25771  ofpreima2  25809  df1stres  25823  df2ndres  25824  iocinif  25894  difioo  25895  iundisj2fi  25904  xrge00  25970  xrge0slmod  26166  ordtconlem1  26208  lmxrge0  26236  esumpfinvallem  26377  measxun2  26478  measvuni  26482  measunl  26484  measinb  26489  eulerpartlemt  26602  eulerpartgbij  26603  probmeasb  26661  cndprobnul  26668  bayesth  26670  ballotlemfp1  26722  ballotlemfval0  26726  ballotlemgun  26755  signstres  26824  subfacp1lem3  26918  subfacp1lem5  26920  pconcon  26968  cvmscld  27010  cvmsss2  27011  dfpred3  27482  epsetlike  27502  pred0  27507  wfi  27515  frind  27551  wfrlem5  27575  frrlem5  27619  nofulllem5  27694  fin2so  28260  ptrest  28269  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ismblfin  28276  cnambfre  28284  asindmre  28323  dvasin  28324  dvreasin  28326  dvreacos  28327  cldbnd  28365  sstotbnd2  28517  bndss  28529  elrfi  28875  coeq0  28935  diophrw  28942  eldioph2lem1  28943  eldioph2lem2  28944  diophin  28956  diophren  28997  dnwech  29246  fnwe2lem2  29249  kelac1  29261  kelac2lem  29262  kelac2  29263  lmhmlnmsplit  29285  pwssplit4  29287  pwfi2f1o  29296  proot1hash  29413  f0rn0  29987  zfregs2VD  31279  iunconlem2  31373  bj-2upln1upl  32100  bj-diagval  32105  l1cvat  32273  pmod2iN  33066  pmodN  33067  pmodl42N  33068  osumcllem3N  33175  osumcllem4N  33176  dihmeetlem19N  34543  dihmeetALTN  34545