Theorem incom 3637

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 456	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3629	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3629	. . 3 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
4	1, 2, 3	3bitr4i 285	. 2 |- ( x e. ( A i^i B ) <-> x e. ( B i^i A ) )
5	4	eqriv 2459	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 375   = wceq 1455   e. wcel 1898   i^i cin 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423

This theorem is referenced by:  ineq2  3640  dfss1  3649  in12  3655  in32  3656  in13  3657  in31  3658  inss2  3665  sslin  3670  inss  3673  indif1  3699  indifcom  3700  indir  3703  dfsymdif3  3720  symdif1OLD  3721  dfrab2  3731  disjr  3818  ssdifin0  3861  difdifdir  3867  uneqdifeq  3868  diftpsn3  4123  iinrab2  4355  iunin1  4357  iinin1  4363  riinn0  4367  rintn0  4386  disjprg  4412  disjxun  4414  inex2  4559  resiun1  5142  dmres  5144  rescom  5148  resima2  5157  xpssres  5158  resindm  5168  resdmdfsn  5169  resopab  5170  imadisj  5206  ndmimaOLD  5225  intirr  5237  djudisj  5283  imainrect  5297  dmresv  5313  resdmres  5345  coeq0  5363  dfpred3  5409  pred0  5429  wfi  5432  ordtri3or  5474  fnresdisj  5708  fnimaeq0  5719  resasplit  5776  fresaun  5777  fresaunres2  5778  fresaunres1  5779  f0rn0  5791  fvun2  5960  fveqressseq  6041  ressnop0  6095  fninfp  6115  fvsnun1  6123  fsnunfv  6128  fveqf1o  6225  orduniss2  6687  offres  6815  curry1  6915  curry2  6918  fpar  6927  fnsuppeq0  6970  wfrlem5  7066  smores3  7098  oacomf1o  7292  ralxpmap  7547  difsnen  7680  domunsncan  7698  domunsn  7748  limensuci  7774  phplem2  7778  pssnn  7816  dif1en  7830  domunfican  7870  marypha1lem  7973  epfrs  8241  zfregs2  8243  tskwe  8410  dif1card  8467  dfac8b  8488  ac10ct  8491  kmlem11  8616  kmlem12  8617  cdacomen  8637  onacda  8653  ackbij1lem14  8689  ackbij1lem16  8691  ackbij1lem18  8693  fin23lem26  8781  fin23lem19  8792  fin23lem30  8798  isf32lem4  8812  isf34lem7  8835  isf34lem6  8836  axdc3lem4  8909  brdom7disj  8985  brdom6disj  8986  fpwwe2lem13  9093  canthp1lem1  9103  grothprim  9285  fzpreddisj  11874  fzdifsuc  11884  fseq1p1m1  11897  hashgval  12550  hashun3  12595  hashfun  12642  hashbclem  12648  xpcoidgend  13088  cotr2  13090  limsupgle  13584  prmreclem2  14910  setsid  15213  ressinbas  15234  wunress  15238  mreexexlem2d  15600  mreexexlem4d  15602  oppcinv  15734  cnvps  16507  pmtrmvd  17146  lsmmod2  17375  lsmdisj3  17382  lsmdisjr  17383  lsmdisj2r  17384  lsmdisj3r  17385  lsmdisj2a  17386  lsmdisj2b  17387  lsmdisj3a  17388  lsmdisj3b  17389  subgdisj2  17391  pj2f  17397  pj1id  17398  frgpuplem  17471  gsummptfzsplitl  17615  dprd2da  17724  dmdprdsplit2lem  17727  dmdprdsplit2  17728  pgpfaclem1  17763  lmhmlsp  18321  pwssplit1  18331  ltbwe  18745  psrbag0  18766  psgndiflemB  19217  pjpm  19320  islindf4  19445  indistopon  20065  fctop  20068  cctop  20070  elcls  20138  mretopd  20157  restin  20231  restsn  20235  restcld  20237  neitr  20245  resstopn  20251  lecldbas  20284  nrmsep  20422  regsep2  20441  isreg2  20442  ordthaus  20449  cmpsublem  20463  cmpsub  20464  hauscmplem  20470  bwth  20474  iuncon  20492  cldllycmp  20559  kgentopon  20602  llycmpkgen2  20614  1stckgen  20618  txkgen  20716  kqcldsat  20797  regr1lem2  20804  fbun  20904  fin1aufil  20996  fclsfnflim  21091  ustexsym  21279  restutopopn  21302  ustuqtop5  21309  ressuss  21327  metreslem  21426  blcld  21569  ressxms  21589  ressms  21590  restmetu  21634  reconn  21895  metdseq0  21920  metnrmlem3  21927  metdseq0OLD  21935  metnrmlem3OLD  21942  unmbl  22540  volun  22547  volinun  22548  iundisj2  22551  icombl  22566  ioombl  22567  uniioombllem2  22589  uniioombllem2OLD  22590  uniioombllem4  22593  dyaddisjlem  22602  dyaddisj  22603  mbfconstlem  22634  mbfeqalem  22647  ismbf3d  22659  itg1addlem5  22707  itgsplitioo  22844  lhop  23017  tdeglem4  23058  vieta1lem2  23313  xrlimcnp  23943  chtdif  24134  ppidif  24139  ppi1  24140  cht1  24141  perfectlem2  24207  rplogsum  24414  perpcom  24807  cusgrasizeindslem2  25251  ex-dif  25922  ococi  27107  orthin  27148  lediri  27239  pjoml2i  27287  pjoml4i  27289  cmcmlem  27293  cmbr3i  27302  cmm2i  27309  cm0  27311  fh1  27320  fh2  27321  cm2j  27322  qlaxr3i  27338  pjclem2  27898  stm1ri  27946  golem1  27973  dmdbr5  28010  mddmd2  28011  cvmdi  28026  mdsldmd1i  28033  csmdsymi  28036  mdexchi  28037  cvexchi  28071  atssma  28080  atomli  28084  atoml2i  28085  atordi  28086  atcvatlem  28087  chirredlem1  28092  chirredlem2  28093  chirredlem3  28094  atcvat4i  28099  atabsi  28103  mdsymlem1  28105  dmdbr6ati  28125  cdj3lem3  28140  inin  28198  difeq  28200  difuncomp  28215  disjdifprg  28234  iundisj2f  28249  disjunsn  28253  imadifxp  28261  fnresin  28277  ofpreima2  28318  df1stres  28333  df2ndres  28334  padct  28356  iocinif  28412  difioo  28413  iundisj2fi  28422  xrge00  28497  xrge0slmod  28656  ordtconlem1  28779  lmxrge0  28807  esumrnmpt2  28938  esumpfinvallem  28944  ldgenpisyslem1  29034  ldgenpisys  29037  measxun2  29081  measvuni  29085  measunl  29087  measinb  29092  carsgclctunlem1  29198  carsgclctunlem2  29200  eulerpartlemt  29253  eulerpartgbij  29254  probmeasb  29312  cndprobnul  29319  bayesth  29321  ballotlemfp1  29373  ballotlemfval0  29377  ballotlemgun  29406  ballotlemgunOLD  29444  signstres  29513  subfacp1lem3  29954  subfacp1lem5  29956  pconcon  30003  cvmscld  30045  cvmsss2  30046  mrsubvrs  30209  mthmpps  30269  frind  30530  frrlem5  30567  nofulllem5  30644  cldbnd  31031  bj-inrab3  31577  bj-2upln1upl  31663  bj-diagval  31690  icoreclin  31805  fin2so  31977  ptrest  31984  poimirlem3  31988  poimirlem11  31996  poimirlem12  31997  poimirlem13  31998  poimirlem14  31999  poimirlem15  32000  poimirlem16  32001  poimirlem18  32003  poimirlem19  32004  poimirlem21  32006  poimirlem22  32007  poimirlem25  32010  poimirlem27  32012  mblfinlem2  32023  mblfinlem3  32024  mblfinlem4  32025  ismblfin  32026  cnambfre  32034  asindmre  32072  dvasin  32073  dvreasin  32075  dvreacos  32076  sstotbnd2  32151  bndss  32163  l1cvat  32666  pmod2iN  33459  pmodN  33460  pmodl42N  33461  osumcllem3N  33568  osumcllem4N  33569  dihmeetlem19N  34938  dihmeetALTN  34940  elrfi  35581  diophrw  35646  eldioph2lem1  35647  eldioph2lem2  35648  diophin  35660  diophren  35701  dnwech  35951  fnwe2lem2  35954  kelac1  35966  kelac2lem  35967  kelac2  35968  lmhmlnmsplit  35990  pwssplit4  35992  pwfi2f1o  35999  proot1hash  36122  rp-fakeuninass  36206  elcnvcnvintab  36233  relintab  36234  elcnvcnvlem  36250  conrel1d  36300  dfrcl2  36311  iunrelexp0  36339  hashnzfz  36713  zfregs2VD  37277  iunconlem2  37372  0in  37431  ssinss2d  37438  iccdifioo  37654  sumnnodd  37748  cncfuni  37802  fouriersw  38133  saliincl  38224  iundjiunlem  38335  iundjiun  38336  caragenuncllem  38371  caragendifcl  38373  isomenndlem  38389  hoidmvlelem2  38456  perfectALTVlem2  38882  prinfzo0  39108  rnghmsscmap2  40248  rnghmsubcsetclem1  40250  rnghmsubcsetc  40252  rngccat  40253  rngcid  40254  rngchomrnghmresALTV  40271  rngcifuestrc  40272  funcrngcsetc  40273  rhmsscmap2  40294  rhmsubcsetclem1  40296  rhmsubcsetc  40298  ringccat  40299  ringcid  40300  rhmsscrnghm  40301  rhmsubcrngclem1  40302  rhmsubcrngc  40304  rngcresringcat  40305  funcringcsetc  40310  rngcrescrhm  40360  rhmsubclem3  40363  rhmsubc  40365  rngcrescrhmALTV  40379  rhmsubcALTVlem3  40382  rhmsubcALTVlem4  40383