Theorem incom 3691

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

Syntax hints:   /\ wa 369   = wceq 1379   e. wcel 1767   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483

This theorem is referenced by:  ineq2  3694  dfss1  3703  in12  3709  in32  3710  in13  3711  in31  3712  inss2  3719  sslin  3724  inss  3727  indif1  3742  indifcom  3743  indir  3746  symdif1  3763  dfrab2  3774  disjr  3868  ssdifin0  3908  difdifdir  3914  uneqdifeq  3915  diftpsn3  4165  iinrab2  4388  iunin1  4390  iinin1  4396  riinn0  4400  rintn0  4416  disjprg  4443  disjxun  4445  inex2  4589  ordtri3or  4910  resiun1  5292  dmres  5294  rescom  5298  resima2  5307  xpssres  5308  resindm  5318  resdmdfsn  5319  resopab  5320  imadisj  5356  ndmima  5373  intirr  5385  djudisj  5434  imainrect  5448  dmresv  5465  resdmres  5498  coeq0  5516  fnresdisj  5691  fnimaeq0  5702  resasplit  5755  fresaun  5756  fresaunres2  5757  fresaunres1  5758  f0rn0  5770  fvun2  5939  ressnop0  6068  fninfp  6088  fvsnun1  6096  fsnunfv  6101  fnsuppeq0OLD  6122  fveqf1o  6193  orduniss2  6652  offres  6779  curry1  6875  curry2  6878  fpar  6887  fnsuppeq0  6928  smores3  7024  oacomf1o  7214  ralxpmap  7468  difsnen  7599  domunsncan  7617  domunsn  7667  limensuci  7693  phplem2  7697  pssnn  7738  dif1enOLD  7752  dif1en  7753  domunfican  7793  marypha1lem  7893  dfsup2OLD  7903  dfsup3OLD  7904  epfrs  8162  zfregs2  8164  tskwe  8331  dif1card  8388  dfac8b  8412  ac10ct  8415  kmlem11  8540  kmlem12  8541  cdacomen  8561  onacda  8577  ackbij1lem14  8613  ackbij1lem16  8615  ackbij1lem18  8617  fin23lem26  8705  fin23lem19  8716  fin23lem30  8722  isf32lem4  8736  isf34lem7  8759  isf34lem6  8760  axdc3lem4  8833  brdom7disj  8909  brdom6disj  8910  fpwwe2lem13  9020  canthp1lem1  9030  grothprim  9212  fzpreddisj  11729  fzdifsuc  11739  fseq1p1m1  11752  hashgval  12376  hashun3  12420  hashfun  12461  hashbclem  12467  limsupgle  13263  prmreclem2  14294  setsid  14531  ressinbas  14551  wunress  14554  mreexexlem2d  14900  mreexexlem4d  14902  oppcinv  15031  cnvps  15699  pmtrmvd  16287  lsmmod2  16500  lsmdisj3  16507  lsmdisjr  16508  lsmdisj2r  16509  lsmdisj3r  16510  lsmdisj2a  16511  lsmdisj2b  16512  lsmdisj3a  16513  lsmdisj3b  16514  subgdisj2  16516  pj2f  16522  pj1id  16523  frgpuplem  16596  gsummptfzsplitl  16756  dprd2da  16893  dmdprdsplit2lem  16896  dmdprdsplit2  16897  pgpfaclem1  16934  lmhmlsp  17495  pwssplit1  17505  ltbwe  17936  psrbag0  17958  psgndiflemB  18431  pjpm  18534  islindf4  18668  indistopon  19296  fctop  19299  cctop  19301  elcls  19368  mretopd  19387  restin  19461  restsn  19465  restcld  19467  neitr  19475  resstopn  19481  lecldbas  19514  nrmsep  19652  regsep2  19671  isreg2  19672  ordthaus  19679  cmpsublem  19693  cmpsub  19694  hauscmplem  19700  bwth  19704  bwthOLD  19705  iuncon  19723  cldllycmp  19790  kgentopon  19802  llycmpkgen2  19814  1stckgen  19818  txkgen  19916  kqcldsat  19997  regr1lem2  20004  fbun  20104  fin1aufil  20196  fclsfnflim  20291  ustexsym  20481  restutopopn  20504  ustuqtop5  20511  ressuss  20529  metreslem  20628  blcld  20771  ressxms  20791  ressms  20792  restmetu  20853  reconn  21096  metdseq0  21121  metnrmlem3  21128  unmbl  21711  volun  21718  volinun  21719  iundisj2  21722  icombl  21737  ioombl  21738  uniioombllem2  21755  uniioombllem4  21758  dyaddisjlem  21767  dyaddisj  21768  mbfconstlem  21799  mbfeqalem  21812  ismbf3d  21824  itg1addlem5  21870  itgsplitioo  22007  lhop  22180  tdeglem4  22221  vieta1lem2  22469  xrlimcnp  23054  chtdif  23188  ppidif  23193  ppi1  23194  cht1  23195  perfectlem2  23261  rplogsum  23468  perpcom  23826  cusgrasizeindslem2  24178  ex-dif  24849  ococi  26027  orthin  26068  lediri  26159  pjoml2i  26207  pjoml4i  26209  cmcmlem  26213  cmbr3i  26222  cmm2i  26229  cm0  26231  fh1  26240  fh2  26241  cm2j  26242  qlaxr3i  26258  pjclem2  26819  stm1ri  26867  golem1  26894  dmdbr5  26931  mddmd2  26932  cvmdi  26947  mdsldmd1i  26954  csmdsymi  26957  mdexchi  26958  cvexchi  26992  atssma  27001  atomli  27005  atoml2i  27006  atordi  27007  atcvatlem  27008  chirredlem1  27013  chirredlem2  27014  chirredlem3  27015  atcvat4i  27020  atabsi  27024  mdsymlem1  27026  dmdbr6ati  27046  cdj3lem3  27061  inin  27115  difeq  27118  disjdifprg  27137  iundisj2f  27150  disjunsn  27154  imadifxp  27159  fnresin  27171  ofpreima2  27208  df1stres  27222  df2ndres  27223  iocinif  27288  difioo  27289  iundisj2fi  27298  xrge00  27364  xrge0slmod  27525  ordtconlem1  27570  lmxrge0  27598  esumpfinvallem  27748  measxun2  27849  measvuni  27853  measunl  27855  measinb  27860  eulerpartlemt  27978  eulerpartgbij  27979  probmeasb  28037  cndprobnul  28044  bayesth  28046  ballotlemfp1  28098  ballotlemfval0  28102  ballotlemgun  28131  signstres  28200  subfacp1lem3  28294  subfacp1lem5  28296  pconcon  28344  cvmscld  28386  cvmsss2  28387  dfpred3  28859  epsetlike  28879  pred0  28884  wfi  28892  frind  28928  wfrlem5  28952  frrlem5  28996  nofulllem5  29071  fin2so  29645  ptrest  29653  mblfinlem2  29657  mblfinlem3  29658  mblfinlem4  29659  ismblfin  29660  cnambfre  29668  asindmre  29707  dvasin  29708  dvreasin  29710  dvreacos  29711  cldbnd  29749  sstotbnd2  29901  bndss  29913  elrfi  30258  diophrw  30324  eldioph2lem1  30325  eldioph2lem2  30326  diophin  30338  diophren  30379  dnwech  30626  fnwe2lem2  30629  kelac1  30641  kelac2lem  30642  kelac2  30643  lmhmlnmsplit  30665  pwssplit4  30667  pwfi2f1o  30676  proot1hash  30793  hashnzfz  30853  iccdifioo  31147  sumnnodd  31200  limcresiooub  31212  limcresioolb  31213  cncfuni  31253  fouriersw  31560  zfregs2VD  32739  iunconlem2  32833  bj-2upln1upl  33681  bj-diagval  33695  l1cvat  33870  pmod2iN  34663  pmodN  34664  pmodl42N  34665  osumcllem3N  34772  osumcllem4N  34773  dihmeetlem19N  36140  dihmeetALTN  36142  conrel1d  36799  xpcoidgend  36802