Theorem incom 3661

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 451	. . 3 |- ( ( x e. A /\ x e. B ) <-> ( x e. B /\ x e. A ) )
2		elin 3655	. . 3 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
3		elin 3655	. . 3 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
4	1, 2, 3	3bitr4i 280	. 2 |- ( x e. ( A i^i B ) <-> x e. ( B i^i A ) )
5	4	eqriv 2425	1 |- ( A i^i B ) = ( B i^i A )

Syntax hints:   /\ wa 370   = wceq 1437   e. wcel 1870   i^i cin 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449

This theorem is referenced by:  ineq2  3664  dfss1  3673  in12  3679  in32  3680  in13  3681  in31  3682  inss2  3689  sslin  3694  inss  3697  indif1  3723  indifcom  3724  indir  3727  dfsymdif3  3744  symdif1OLD  3745  dfrab2  3755  disjr  3840  ssdifin0  3883  difdifdir  3889  uneqdifeq  3890  diftpsn3  4141  iinrab2  4365  iunin1  4367  iinin1  4373  riinn0  4377  rintn0  4396  disjprg  4422  disjxun  4424  inex2  4567  resiun1  5143  dmres  5145  rescom  5149  resima2  5158  xpssres  5159  resindm  5169  resdmdfsn  5170  resopab  5171  imadisj  5207  ndmimaOLD  5226  intirr  5238  djudisj  5284  imainrect  5298  dmresv  5314  resdmres  5346  coeq0  5364  dfpred3  5409  pred0  5429  wfi  5432  ordtri3or  5474  fnresdisj  5704  fnimaeq0  5715  resasplit  5770  fresaun  5771  fresaunres2  5772  fresaunres1  5773  f0rn0  5785  fvun2  5953  fveqressseq  6033  ressnop0  6086  fninfp  6106  fvsnun1  6114  fsnunfv  6119  fveqf1o  6215  orduniss2  6674  offres  6802  curry1  6899  curry2  6902  fpar  6911  fnsuppeq0  6954  wfrlem5  7048  smores3  7080  oacomf1o  7274  ralxpmap  7529  difsnen  7660  domunsncan  7678  domunsn  7728  limensuci  7754  phplem2  7758  pssnn  7796  dif1en  7810  domunfican  7850  marypha1lem  7953  epfrs  8214  zfregs2  8216  tskwe  8383  dif1card  8440  dfac8b  8460  ac10ct  8463  kmlem11  8588  kmlem12  8589  cdacomen  8609  onacda  8625  ackbij1lem14  8661  ackbij1lem16  8663  ackbij1lem18  8665  fin23lem26  8753  fin23lem19  8764  fin23lem30  8770  isf32lem4  8784  isf34lem7  8807  isf34lem6  8808  axdc3lem4  8881  brdom7disj  8957  brdom6disj  8958  fpwwe2lem13  9066  canthp1lem1  9076  grothprim  9258  fzpreddisj  11843  fzdifsuc  11853  fseq1p1m1  11866  hashgval  12515  hashun3  12560  hashfun  12604  hashbclem  12610  xpcoidgend  13018  cotr2  13020  limsupgle  13513  prmreclem2  14815  setsid  15118  ressinbas  15138  wunress  15142  mreexexlem2d  15493  mreexexlem4d  15495  oppcinv  15627  cnvps  16400  pmtrmvd  17039  lsmmod2  17252  lsmdisj3  17259  lsmdisjr  17260  lsmdisj2r  17261  lsmdisj3r  17262  lsmdisj2a  17263  lsmdisj2b  17264  lsmdisj3a  17265  lsmdisj3b  17266  subgdisj2  17268  pj2f  17274  pj1id  17275  frgpuplem  17348  gsummptfzsplitl  17492  dprd2da  17601  dmdprdsplit2lem  17604  dmdprdsplit2  17605  pgpfaclem1  17640  lmhmlsp  18198  pwssplit1  18208  ltbwe  18622  psrbag0  18643  psgndiflemB  19090  pjpm  19193  islindf4  19318  indistopon  19938  fctop  19941  cctop  19943  elcls  20011  mretopd  20030  restin  20104  restsn  20108  restcld  20110  neitr  20118  resstopn  20124  lecldbas  20157  nrmsep  20295  regsep2  20314  isreg2  20315  ordthaus  20322  cmpsublem  20336  cmpsub  20337  hauscmplem  20343  bwth  20347  iuncon  20365  cldllycmp  20432  kgentopon  20475  llycmpkgen2  20487  1stckgen  20491  txkgen  20589  kqcldsat  20670  regr1lem2  20677  fbun  20777  fin1aufil  20869  fclsfnflim  20964  ustexsym  21152  restutopopn  21175  ustuqtop5  21182  ressuss  21200  metreslem  21299  blcld  21442  ressxms  21462  ressms  21463  restmetu  21507  reconn  21748  metdseq0  21773  metnrmlem3  21780  unmbl  22359  volun  22366  volinun  22367  iundisj2  22370  icombl  22385  ioombl  22386  uniioombllem2  22408  uniioombllem2OLD  22409  uniioombllem4  22412  dyaddisjlem  22421  dyaddisj  22422  mbfconstlem  22453  mbfeqalem  22466  ismbf3d  22478  itg1addlem5  22526  itgsplitioo  22663  lhop  22836  tdeglem4  22877  vieta1lem2  23123  xrlimcnp  23750  chtdif  23939  ppidif  23944  ppi1  23945  cht1  23946  perfectlem2  24012  rplogsum  24219  perpcom  24606  cusgrasizeindslem2  25038  ex-dif  25709  ococi  26884  orthin  26925  lediri  27016  pjoml2i  27064  pjoml4i  27066  cmcmlem  27070  cmbr3i  27079  cmm2i  27086  cm0  27088  fh1  27097  fh2  27098  cm2j  27099  qlaxr3i  27115  pjclem2  27675  stm1ri  27723  golem1  27750  dmdbr5  27787  mddmd2  27788  cvmdi  27803  mdsldmd1i  27810  csmdsymi  27813  mdexchi  27814  cvexchi  27848  atssma  27857  atomli  27861  atoml2i  27862  atordi  27863  atcvatlem  27864  chirredlem1  27869  chirredlem2  27870  chirredlem3  27871  atcvat4i  27876  atabsi  27880  mdsymlem1  27882  dmdbr6ati  27902  cdj3lem3  27917  inin  27976  difeq  27978  difuncomp  27996  disjdifprg  28015  iundisj2f  28030  disjunsn  28034  imadifxp  28042  fnresin  28059  ofpreima2  28100  df1stres  28115  df2ndres  28116  padct  28141  iocinif  28190  difioo  28191  iundisj2fi  28200  xrge00  28276  xrge0slmod  28437  ordtconlem1  28560  lmxrge0  28588  esumrnmpt2  28719  esumpfinvallem  28725  ldgenpisyslem1  28815  ldgenpisys  28818  measxun2  28862  measvuni  28866  measunl  28868  measinb  28873  carsgclctunlem1  28969  carsgclctunlem2  28971  eulerpartlemt  29021  eulerpartgbij  29022  probmeasb  29080  cndprobnul  29087  bayesth  29089  ballotlemfp1  29141  ballotlemfval0  29145  ballotlemgun  29174  signstres  29243  subfacp1lem3  29684  subfacp1lem5  29686  pconcon  29733  cvmscld  29775  cvmsss2  29776  mrsubvrs  29939  mthmpps  29999  frind  30259  frrlem5  30296  nofulllem5  30371  cldbnd  30758  bj-inrab3  31273  bj-2upln1upl  31358  bj-diagval  31381  icoreclin  31485  fin2so  31626  ptrest  31633  poimirlem3  31637  poimirlem11  31645  poimirlem12  31646  poimirlem13  31647  poimirlem14  31648  poimirlem15  31649  poimirlem16  31650  poimirlem18  31652  poimirlem19  31653  poimirlem21  31655  poimirlem22  31656  poimirlem25  31659  poimirlem27  31661  mblfinlem2  31672  mblfinlem3  31673  mblfinlem4  31674  ismblfin  31675  cnambfre  31683  asindmre  31721  dvasin  31722  dvreasin  31724  dvreacos  31725  sstotbnd2  31800  bndss  31812  l1cvat  32320  pmod2iN  33113  pmodN  33114  pmodl42N  33115  osumcllem3N  33222  osumcllem4N  33223  dihmeetlem19N  34592  dihmeetALTN  34594  elrfi  35235  diophrw  35300  eldioph2lem1  35301  eldioph2lem2  35302  diophin  35314  diophren  35355  dnwech  35602  fnwe2lem2  35605  kelac1  35617  kelac2lem  35618  kelac2  35619  lmhmlnmsplit  35641  pwssplit4  35643  pwfi2f1o  35650  proot1hash  35766  rp-fakeuninass  35850  conrel1d  35884  dfrcl2  35895  iunrelexp0  35923  hashnzfz  36296  zfregs2VD  36867  iunconlem2  36962  0in  37024  ssinss2d  37031  iccdifioo  37191  sumnnodd  37272  cncfuni  37326  fouriersw  37653  saliincl  37723  iundjiunlem  37796  iundjiun  37797  caragenuncllem  37832  caragendifcl  37834  perfectALTVlem2  38224  rnghmsscmap2  38723  rnghmsubcsetclem1  38725  rnghmsubcsetc  38727  rngccat  38728  rngcid  38729  rngchomrnghmresALTV  38746  rngcifuestrc  38747  funcrngcsetc  38748  rhmsscmap2  38769  rhmsubcsetclem1  38771  rhmsubcsetc  38773  ringccat  38774  ringcid  38775  rhmsscrnghm  38776  rhmsubcrngclem1  38777  rhmsubcrngc  38779  rngcresringcat  38780  funcringcsetc  38785  rngcrescrhm  38835  rhmsubclem3  38838  rhmsubc  38840  rngcrescrhmALTV  38854  rhmsubcALTVlem3  38857  rhmsubcALTVlem4  38858