Theorem incom 3493

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 438	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3490	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3490	. . 3 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
4	1, 2, 3	3bitr4i 269	. 2 |- ( x e. ( A i^i B ) <-> x e. ( B i^i A ) )
5	4	eqriv 2401	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 359   = wceq 1649   e. wcel 1721   i^i cin 3279

This theorem is referenced by:  ineq2  3496  dfss1  3505  in12  3512  in32  3513  in13  3514  in31  3515  inss2  3522  sslin  3527  inss  3530  indif1  3545  indifcom  3546  indir  3549  symdif1  3566  dfrab2  3576  disjr  3629  ssdifin0  3669  difdifdir  3675  uneqdifeq  3676  diftpsn3  3897  iinrab2  4114  iunin1  4116  iinin1  4122  riinn0  4125  rintn0  4141  disjprg  4168  disjxun  4170  inex2  4305  ordtri3or  4573  orduniss2  4772  resiun1  5124  dmres  5126  rescom  5130  resima2  5138  xpssres  5139  resopab  5146  imadisj  5182  ndmima  5200  intirr  5211  djudisj  5256  imainrect  5271  dmresv  5288  resdmres  5320  fnresdisj  5514  fnimaeq0  5525  resasplit  5572  fresaun  5573  fresaunres2  5574  fresaunres1  5575  fvun2  5754  ressnop0  5872  fvsnun1  5887  fsnunfv  5892  fnsuppeq0  5912  fveqf1o  5988  offres  6278  curry1  6397  curry2  6400  fpar  6409  smores3  6574  oacomf1o  6767  difsnen  7149  domunsncan  7167  domunsn  7216  limensuci  7242  phplem2  7246  pssnn  7286  dif1enOLD  7299  dif1en  7300  domunfican  7338  marypha1lem  7396  dfsup2OLD  7406  dfsup3OLD  7407  epfrs  7623  zfregs2  7625  tskwe  7793  dif1card  7848  dfac8b  7868  ac10ct  7871  kmlem11  7996  kmlem12  7997  cdacomen  8017  onacda  8033  ackbij1lem14  8069  ackbij1lem16  8071  ackbij1lem18  8073  fin23lem26  8161  fin23lem19  8172  fin23lem30  8178  isf32lem4  8192  isf34lem7  8215  isf34lem6  8216  axdc3lem4  8289  brdom7disj  8365  brdom6disj  8366  fpwwe2lem13  8473  canthp1lem1  8483  grothprim  8665  fseq1p1m1  11077  hashgval  11576  hashun3  11613  hashfun  11655  hashbclem  11656  limsupgle  12226  prmreclem2  13240  setsid  13463  ressinbas  13480  wunress  13483  mreexexlem2d  13825  mreexexlem4d  13827  oppcinv  13956  cnvps  14599  lsmmod2  15263  lsmdisj3  15270  lsmdisjr  15271  lsmdisj2r  15272  lsmdisj3r  15273  lsmdisj2a  15274  lsmdisj2b  15275  lsmdisj3a  15276  lsmdisj3b  15277  subgdisj2  15279  pj2f  15285  pj1id  15286  frgpuplem  15359  dprd2da  15555  dmdprdsplit2lem  15558  dmdprdsplit2  15559  pgpfaclem1  15594  lmhmlsp  16080  ltbwe  16488  psrbag0  16509  pjpm  16890  indistopon  17020  fctop  17023  cctop  17025  elcls  17092  mretopd  17111  restin  17184  restsn  17188  restcld  17190  neitr  17198  resstopn  17204  lecldbas  17237  nrmsep  17375  regsep2  17394  isreg2  17395  ordthaus  17402  cmpsublem  17416  cmpsub  17417  hauscmplem  17423  iuncon  17444  cldllycmp  17511  kgentopon  17523  llycmpkgen2  17535  1stckgen  17539  txkgen  17637  kqcldsat  17718  regr1lem2  17725  fbun  17825  fin1aufil  17917  fclsfnflim  18012  ustexsym  18198  restutopopn  18221  ustuqtop5  18228  ressuss  18246  metreslem  18345  blcld  18488  ressxms  18508  ressms  18509  restmetu  18570  reconn  18812  metdseq0  18837  metnrmlem3  18844  unmbl  19385  volun  19392  volinun  19393  iundisj2  19396  icombl  19411  ioombl  19412  uniioombllem2  19428  uniioombllem4  19431  dyaddisjlem  19440  dyaddisj  19441  mbfconstlem  19474  mbfeqalem  19487  ismbf3d  19499  itg1addlem5  19545  itgsplitioo  19682  lhop  19853  tdeglem4  19936  vieta1lem2  20181  xrlimcnp  20760  chtdif  20894  ppidif  20899  ppi1  20900  cht1  20901  perfectlem2  20967  rplogsum  21174  cusgrasizeindslem2  21436  ex-dif  21684  ococi  22860  orthin  22901  lediri  22992  pjoml2i  23040  pjoml4i  23042  cmcmlem  23046  cmbr3i  23055  cmm2i  23062  cm0  23064  fh1  23073  fh2  23074  cm2j  23075  qlaxr3i  23091  pjclem2  23652  stm1ri  23700  golem1  23727  dmdbr5  23764  mddmd2  23765  cvmdi  23780  mdsldmd1i  23787  csmdsymi  23790  mdexchi  23791  cvexchi  23825  atssma  23834  atomli  23838  atoml2i  23839  atordi  23840  atcvatlem  23841  chirredlem1  23846  chirredlem2  23847  chirredlem3  23848  atcvat4i  23853  atabsi  23857  mdsymlem1  23859  dmdbr6ati  23879  cdj3lem3  23894  inin  23949  difeq  23951  disjdifprg  23970  iundisj2f  23983  imadifxp  23991  df1stres  24044  df2ndres  24045  iocinif  24097  difioo  24098  iundisj2fi  24106  xrge00  24161  lmxrge0  24290  esumpfinvallem  24417  measxun2  24517  measvuni  24521  measunl  24523  measinb  24528  sibfof  24607  probmeasb  24641  cndprobnul  24648  bayesth  24650  ballotlemfp1  24702  ballotlemfval0  24706  ballotlemgun  24735  subfacp1lem3  24821  subfacp1lem5  24823  pconcon  24871  cvmscld  24913  cvmsss2  24914  epsetlike  25408  pred0  25413  wfi  25421  frind  25457  wfrlem5  25474  frrlem5  25499  nofulllem5  25574  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  cnambfre  26154  cldbnd  26219  sstotbnd2  26373  bndss  26385  fninfp  26625  ralxpmap  26632  elrfi  26638  coeq0  26700  diophrw  26707  eldioph2lem1  26708  eldioph2lem2  26709  diophin  26721  diophren  26764  dnwech  27013  fnwe2lem2  27016  kelac1  27029  kelac2lem  27030  kelac2  27031  lmhmlnmsplit  27053  pwssplit1  27056  pwssplit4  27059  pwfi2f1o  27128  islindf4  27176  pmtrmvd  27266  proot1hash  27387  zfregs2VD  28662  l1cvat  29538  pmod2iN  30331  pmodN  30332  pmodl42N  30333  osumcllem3N  30440  osumcllem4N  30441  dihmeetlem19N  31808  dihmeetALTN  31810

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287