Theorem incom 4034

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 454	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
2		elin 4025	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
3		elin 4025	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐴) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
4	1, 2, 3	3bitr4i 295	. 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥 ∈ (𝐵 ∩ 𝐴))
5	4	eqriv 2822	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   ∧ wa 386   = wceq 1656   ∈ wcel 2164   ∩ cin 3797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805

This theorem is referenced by:  ineq2  4037  sseqin2  4046  in12  4051  in32  4052  in13  4053  in31  4054  inss2  4060  sslin  4065  inss  4069  indif1  4103  indifcom  4104  indir  4107  dfsymdif3  4124  dfrab2  4134  0in  4196  disjr  4244  ssdifin0  4275  difdifdir  4281  uneqdifeq  4282  disjtp2  4472  iinrab2  4805  iunin1  4807  iinin1  4813  riinn0  4817  disjprg  4871  disjxun  4873  inex2  5027  rescom  5663  resindm  5685  resdmdfsn  5686  resopab  5687  imadisj  5729  intirr  5760  djudisj  5806  imainrect  5820  dmresv  5838  resdmres  5870  coeq0  5889  dfpred3  5934  wfi  5957  ordtri3or  5999  fnresdisj  6238  fnimaeq0  6250  resasplit  6315  fresaun  6316  fresaunres2  6317  fresaunres1  6318  f0rn0  6331  fvun2  6521  fveqressseq  6609  ressnop0  6676  fninfp  6697  fvsnun1  6707  fvsnun1OLD  6709  fsnunfv  6714  fveqf1o  6817  orduniss2  7299  offres  7428  curry1  7538  curry2  7541  fpar  7550  wfrlem5  7690  smores3  7721  oacomf1o  7917  ralxpmap  8180  difsnen  8317  domunsncan  8335  domunsn  8385  limensuci  8411  phplem2  8415  pssnn  8453  dif1en  8468  domunfican  8508  marypha1lem  8614  zfregfr  8785  epfrs  8891  zfregs2  8893  djuin  9064  tskwe  9096  dif1card  9153  dfac8b  9174  ac10ct  9177  kmlem11  9304  kmlem12  9305  cdacomen  9325  onacda  9341  ackbij1lem14  9377  ackbij1lem16  9379  ackbij1lem18  9381  fin23lem26  9469  fin23lem19  9480  fin23lem30  9486  isf32lem4  9500  isf34lem7  9523  isf34lem6  9524  axdc3lem4  9597  brdom7disj  9675  brdom6disj  9676  fpwwe2lem13  9786  canthp1lem1  9796  grothprim  9978  fzpreddisj  12690  fzdifsuc  12701  fseq1p1m1  12715  prinfzo0  12809  hashgval  13420  hashun3  13470  hashfun  13520  hashbclem  13532  xpcoidgend  14100  cotr2  14102  limsupgle  14592  prmreclem2  15999  setsdm  16263  setsfun  16264  setsfun0  16265  setsid  16284  ressinbas  16306  wunress  16311  mreexexlem2d  16665  mreexexlem4d  16667  oppcinv  16799  cnvps  17572  pmtrmvd  18233  lsmmod2  18447  lsmdisj3  18454  lsmdisjr  18455  lsmdisj2r  18456  lsmdisj3r  18457  lsmdisj2a  18458  lsmdisj2b  18459  lsmdisj3a  18460  lsmdisj3b  18461  subgdisj2  18463  pj2f  18469  pj1id  18470  frgpuplem  18545  gsummptfzsplitl  18693  dprd2da  18802  dmdprdsplit2lem  18805  dmdprdsplit2  18806  pgpfaclem1  18841  lmhmlsp  19415  pwssplit1  19425  ltbwe  19840  psrbag0  19861  cnfldfun  20125  psgndiflemB  20313  pjpm  20422  islindf4  20551  elcls  21255  mretopd  21274  restin  21348  restcld  21354  neitr  21362  resstopn  21368  lecldbas  21401  nrmsep  21539  regsep2  21558  isreg2  21559  ordthaus  21566  cmpsublem  21580  cmpsub  21581  hauscmplem  21587  bwth  21591  iunconn  21609  cldllycmp  21676  kgentopon  21719  llycmpkgen2  21731  1stckgen  21735  txkgen  21833  kqcldsat  21914  regr1lem2  21921  fbun  22021  fin1aufil  22113  fclsfnflim  22208  ustexsym  22396  restutopopn  22419  ustuqtop5  22426  ressuss  22444  metreslem  22544  blcld  22687  ressxms  22707  ressms  22708  restmetu  22752  reconn  23008  metdseq0  23034  metnrmlem3  23041  unmbl  23710  volun  23718  volinun  23719  iundisj2  23722  icombl  23737  ioombl  23738  uniioombllem2  23756  uniioombllem4  23759  dyaddisjlem  23768  dyaddisj  23769  mbfconstlem  23800  mbfeqalem2  23815  ismbf3d  23827  itg1addlem5  23873  itgsplitioo  24010  lhop  24185  tdeglem4  24226  vieta1lem2  24472  xrlimcnp  25115  perfectlem2  25375  rplogsum  25636  perpcom  26032  vtxdgoddnumeven  26858  ex-dif  27834  ococi  28815  orthin  28856  lediri  28947  pjoml2i  28995  pjoml4i  28997  cmcmlem  29001  cmbr3i  29010  cmm2i  29017  cm0  29019  fh1  29028  fh2  29029  cm2j  29030  qlaxr3i  29046  pjclem2  29606  stm1ri  29654  golem1  29681  dmdbr5  29718  mddmd2  29719  cvmdi  29734  mdsldmd1i  29741  csmdsymi  29744  mdexchi  29745  cvexchi  29779  atssma  29788  atomli  29792  atoml2i  29793  atordi  29794  atcvatlem  29795  chirredlem1  29800  chirredlem2  29801  chirredlem3  29802  atcvat4i  29807  atabsi  29811  mdsymlem1  29813  dmdbr6ati  29833  cdj3lem3  29848  inin  29896  difeq  29899  difuncomp  29913  disjdifprg  29931  iundisj2f  29946  disjunsn  29950  imadifxp  29957  fnresin  29975  df1stres  30025  df2ndres  30026  padct  30041  iocinif  30086  difioo  30087  iundisj2fi  30099  xrge00  30227  xrge0slmod  30385  lmxrge0  30539  esumrnmpt2  30671  esumpfinvallem  30677  ldgenpisyslem1  30767  ldgenpisys  30770  measxun2  30814  measunl  30820  carsgclctunlem1  30920  carsgclctunlem2  30922  eulerpartlemt  30974  eulerpartgbij  30975  probmeasb  31034  bayesth  31043  ballotlemfp1  31095  ballotlemfval0  31099  signstres  31196  hashreprin  31243  reprfz1  31247  chtvalz  31252  breprexpnat  31257  subfacp1lem3  31706  subfacp1lem5  31708  pconnconn  31755  cvmscld  31797  cvmsss2  31798  mrsubvrs  31961  mthmpps  32021  frpoind  32274  frind  32277  frrlem5  32318  nosupbnd2lem1  32395  noetalem2  32398  noetalem3  32399  cldbnd  32854  bj-inrab3  33444  bj-2upln1upl  33529  bj-sscon  33531  bj-rest0  33564  bj-0int  33573  bj-diagval  33614  icoreclin  33745  fin2so  33934  ptrest  33947  poimirlem3  33951  poimirlem11  33959  poimirlem12  33960  poimirlem13  33961  poimirlem14  33962  poimirlem15  33963  poimirlem16  33964  poimirlem18  33966  poimirlem19  33967  poimirlem21  33969  poimirlem22  33970  poimirlem27  33975  mblfinlem3  33987  mblfinlem4  33988  ismblfin  33989  cnambfre  33996  asindmre  34033  dvasin  34034  dvreasin  34036  dvreacos  34037  sstotbnd2  34110  bndss  34122  ineqcom  34556  inres2  34558  inex2ALTV  34648  redss3  34912  l1cvat  35125  pmod2iN  35919  pmodN  35920  pmodl42N  35921  osumcllem3N  36028  osumcllem4N  36029  dihmeetlem19N  37395  dihmeetALTN  37397  elrfi  38096  diophrw  38161  eldioph2lem1  38162  eldioph2lem2  38163  diophin  38175  diophren  38216  dnwech  38456  fnwe2lem2  38459  kelac1  38471  kelac2lem  38472  kelac2  38473  lmhmlnmsplit  38495  pwssplit4  38497  pwfi2f1o  38504  proot1hash  38616  rp-fakeuninass  38698  elcnvcnvintab  38724  relintab  38725  elcnvcnvlem  38741  conrel1d  38791  dfrcl2  38802  iunrelexp0  38830  ntrk0kbimka  39172  neicvgbex  39245  hashnzfz  39354  zfregs2VD  39890  iunconnlem2  39984  ssinss2d  40040  restuni4  40114  restuni6  40115  iccdifioo  40531  uzinico2  40578  sumnnodd  40651  limsupvaluz  40729  cncfuni  40888  fouriersw  41236  saliincl  41330  iundjiunlem  41461  iundjiun  41462  caragenuncllem  41514  caragendifcl  41516  isomenndlem  41532  hoidmvlelem2  41598  smflimlem1  41767  dfss7  42174  perfectALTVlem2  42475  rnghmsscmap2  42834  rnghmsubcsetclem1  42836  rnghmsubcsetc  42838  rngccat  42839  rngcid  42840  rngchomrnghmresALTV  42857  rngcifuestrc  42858  funcrngcsetc  42859  rhmsscmap2  42880  rhmsubcsetclem1  42882  rhmsubcsetc  42884  ringccat  42885  ringcid  42886  rhmsscrnghm  42887  rhmsubcrngclem1  42888  rhmsubcrngc  42890  rngcresringcat  42891  funcringcsetc  42896  rngcrescrhm  42946  rhmsubclem3  42949  rhmsubc  42951  rngcrescrhmALTV  42964  rhmsubcALTVlem3  42967  rhmsubcALTVlem4  42968