Theorem incom 3767

Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
incom	⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Proof of Theorem incom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ancom 465	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
2		elin 3758	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 3758	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
4	1, 2, 3	3bitr4i 291	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴))
5	4	eqriv 2607	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  ineq2  3770  sseqin2  3779  dfss1OLD  3780  in12  3786  in32  3787  in13  3788  in31  3789  inss2  3796  sslin  3801  inss  3804  indif1  3830  indifcom  3831  indir  3834  dfsymdif3  3852  dfrab2  3862  0in  3921  disjr  3970  ssdifin0  4002  difdifdir  4008  uneqdifeq  4009  uneqdifeqOLD  4010  diftpsn3OLD  4274  iinrab2  4519  iunin1  4521  iinin1  4527  riinn0  4531  disjprg  4578  disjxun  4581  inex2  4728  resiun1OLD  5337  dmres  5339  rescom  5343  resima2OLD  5353  resindm  5364  resdmdfsn  5365  resopab  5366  imadisj  5403  intirr  5433  djudisj  5480  imainrect  5494  dmresv  5511  resdmres  5543  coeq0  5561  dfpred3  5607  wfi  5630  ordtri3or  5672  fnresdisj  5915  fnimaeq0  5926  resasplit  5987  fresaun  5988  fresaunres2  5989  fresaunres1  5990  f0rn0  6003  fvun2  6180  fveqressseq  6263  ressnop0  6325  fninfp  6345  fvsnun1  6353  fsnunfv  6358  fveqf1o  6457  orduniss2  6925  offres  7054  curry1  7156  curry2  7159  fpar  7168  wfrlem5  7306  smores3  7337  oacomf1o  7532  ralxpmap  7793  difsnen  7927  domunsncan  7945  domunsn  7995  limensuci  8021  phplem2  8025  pssnn  8063  dif1en  8078  domunfican  8118  marypha1lem  8222  zfregfr  8392  epfrs  8490  zfregs2  8492  tskwe  8659  dif1card  8716  dfac8b  8737  ac10ct  8740  kmlem11  8865  kmlem12  8866  cdacomen  8886  onacda  8902  ackbij1lem14  8938  ackbij1lem16  8940  ackbij1lem18  8942  fin23lem26  9030  fin23lem19  9041  fin23lem30  9047  isf32lem4  9061  isf34lem7  9084  isf34lem6  9085  axdc3lem4  9158  brdom7disj  9234  brdom6disj  9235  fpwwe2lem13  9343  canthp1lem1  9353  grothprim  9535  fzpreddisj  12260  fzdifsuc  12270  fseq1p1m1  12283  hashgval  12982  hashun3  13034  hashfun  13084  hashbclem  13093  xpcoidgend  13562  cotr2  13564  limsupgle  14056  prmreclem2  15459  setsdm  15724  setsfun  15725  setsfun0  15726  setsid  15742  ressinbas  15763  wunress  15767  mreexexlem2d  16128  mreexexlem4d  16130  oppcinv  16263  cnvps  17035  pmtrmvd  17699  lsmmod2  17912  lsmdisj3  17919  lsmdisjr  17920  lsmdisj2r  17921  lsmdisj3r  17922  lsmdisj2a  17923  lsmdisj2b  17924  lsmdisj3a  17925  lsmdisj3b  17926  subgdisj2  17928  pj2f  17934  pj1id  17935  frgpuplem  18008  gsummptfzsplitl  18156  dprd2da  18264  dmdprdsplit2lem  18267  dmdprdsplit2  18268  pgpfaclem1  18303  lmhmlsp  18870  pwssplit1  18880  ltbwe  19293  psrbag0  19315  psgndiflemB  19765  pjpm  19871  islindf4  19996  elcls  20687  mretopd  20706  restin  20780  restcld  20786  neitr  20794  resstopn  20800  lecldbas  20833  nrmsep  20971  regsep2  20990  isreg2  20991  ordthaus  20998  cmpsublem  21012  cmpsub  21013  hauscmplem  21019  bwth  21023  iuncon  21041  cldllycmp  21108  kgentopon  21151  llycmpkgen2  21163  1stckgen  21167  txkgen  21265  kqcldsat  21346  regr1lem2  21353  fbun  21454  fin1aufil  21546  fclsfnflim  21641  ustexsym  21829  restutopopn  21852  ustuqtop5  21859  ressuss  21877  metreslem  21977  blcld  22120  ressxms  22140  ressms  22141  restmetu  22185  reconn  22439  metdseq0  22465  metnrmlem3  22472  unmbl  23112  volun  23120  volinun  23121  iundisj2  23124  icombl  23139  ioombl  23140  uniioombllem2  23157  uniioombllem4  23160  dyaddisjlem  23169  dyaddisj  23170  mbfconstlem  23202  mbfeqalem  23215  ismbf3d  23227  itg1addlem5  23273  itgsplitioo  23410  lhop  23583  tdeglem4  23624  vieta1lem2  23870  xrlimcnp  24495  perfectlem2  24755  rplogsum  25016  perpcom  25408  cusgrasizeindslem1  26002  ex-dif  26672  ococi  27648  orthin  27689  lediri  27780  pjoml2i  27828  pjoml4i  27830  cmcmlem  27834  cmbr3i  27843  cmm2i  27850  cm0  27852  fh1  27861  fh2  27862  cm2j  27863  qlaxr3i  27879  pjclem2  28439  stm1ri  28487  golem1  28514  dmdbr5  28551  mddmd2  28552  cvmdi  28567  mdsldmd1i  28574  csmdsymi  28577  mdexchi  28578  cvexchi  28612  atssma  28621  atomli  28625  atoml2i  28626  atordi  28627  atcvatlem  28628  chirredlem1  28633  chirredlem2  28634  chirredlem3  28635  atcvat4i  28640  atabsi  28644  mdsymlem1  28646  dmdbr6ati  28666  cdj3lem3  28681  inin  28737  difeq  28739  difuncomp  28752  disjdifprg  28770  iundisj2f  28785  disjunsn  28789  imadifxp  28796  fnresin  28812  df1stres  28864  df2ndres  28865  padct  28885  iocinif  28933  difioo  28934  iundisj2fi  28943  xrge00  29017  xrge0slmod  29175  lmxrge0  29326  esumrnmpt2  29457  esumpfinvallem  29463  ldgenpisyslem1  29553  ldgenpisys  29556  measxun2  29600  measunl  29606  carsgclctunlem1  29706  carsgclctunlem2  29708  eulerpartlemt  29760  eulerpartgbij  29761  probmeasb  29819  bayesth  29828  ballotlemfp1  29880  ballotlemfval0  29884  signstres  29978  subfacp1lem3  30418  subfacp1lem5  30420  pconcon  30467  cvmscld  30509  cvmsss2  30510  mrsubvrs  30673  mthmpps  30733  frind  30984  frrlem5  31028  nofulllem5  31105  cldbnd  31491  bj-inrab3  32117  bj-2upln1upl  32205  bj-rest0  32227  bj-diagval  32267  icoreclin  32381  fin2so  32566  ptrest  32578  poimirlem3  32582  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem18  32597  poimirlem19  32598  poimirlem21  32600  poimirlem22  32601  poimirlem27  32606  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  cnambfre  32628  asindmre  32665  dvasin  32666  dvreasin  32668  dvreacos  32669  sstotbnd2  32743  bndss  32755  l1cvat  33360  pmod2iN  34153  pmodN  34154  pmodl42N  34155  osumcllem3N  34262  osumcllem4N  34263  dihmeetlem19N  35632  dihmeetALTN  35634  elrfi  36275  diophrw  36340  eldioph2lem1  36341  eldioph2lem2  36342  diophin  36354  diophren  36395  dnwech  36636  fnwe2lem2  36639  kelac1  36651  kelac2lem  36652  kelac2  36653  lmhmlnmsplit  36675  pwssplit4  36677  pwfi2f1o  36684  proot1hash  36797  rp-fakeuninass  36881  elcnvcnvintab  36907  relintab  36908  elcnvcnvlem  36924  conrel1d  36974  dfrcl2  36985  iunrelexp0  37013  ntrkbimka  37356  ntrk0kbimka  37357  neicvgbex  37430  hashnzfz  37541  zfregs2VD  38098  iunconlem2  38193  ssinss2d  38253  restuni4  38336  restuni6  38337  iccdifioo  38588  sumnnodd  38697  cncfuni  38772  fouriersw  39124  saliincl  39221  iundjiunlem  39352  iundjiun  39353  caragenuncllem  39402  caragendifcl  39404  isomenndlem  39420  hoidmvlelem2  39486  smflimlem1  39657  perfectALTVlem2  40165  prinfzo0  40363  rnghmsscmap2  41765  rnghmsubcsetclem1  41767  rnghmsubcsetc  41769  rngccat  41770  rngcid  41771  rngchomrnghmresALTV  41788  rngcifuestrc  41789  funcrngcsetc  41790  rhmsscmap2  41811  rhmsubcsetclem1  41813  rhmsubcsetc  41815  ringccat  41816  ringcid  41817  rhmsscrnghm  41818  rhmsubcrngclem1  41819  rhmsubcrngc  41821  rngcresringcat  41822  funcringcsetc  41827  rngcrescrhm  41877  rhmsubclem3  41880  rhmsubc  41882  rngcrescrhmALTV  41896  rhmsubcALTVlem3  41899  rhmsubcALTVlem4  41900