Theorem incom 4128

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

Assertion

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

Proof of Theorem incom

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rabswap 3436	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
2		dfin5 3889	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
3		dfin5 3889	. 2 ⊢ (𝐵 ∩ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
4	1, 2, 3	3eqtr4i 2831	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   = wceq 1538   ∈ wcel 2111  {crab 3110   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-rab 3115  df-in 3888

This theorem is referenced by:  ineq2  4133  sseqin2  4142  in12  4147  in32  4148  in13  4149  in31  4150  inss2  4156  sslin  4161  inss  4165  dfss7  4167  indif1  4198  indifcom  4199  indir  4202  dfsymdif3  4221  dfrab2  4231  0in  4301  disjr  4357  ssdifin0  4389  difdifdir  4395  uneqdifeq  4396  disjtp2  4612  iinrab2  4955  iunin1  4957  iinin1  4964  riinn0  4968  disjprgw  5025  disjprg  5026  disjxun  5028  inex2  5186  inex2g  5188  rescom  5844  resindm  5867  resdmdfsn  5868  resopab  5869  imadisj  5915  intirr  5945  djudisj  5991  imainrect  6005  dmresv  6024  resdmres  6056  coeq0  6075  dfpred3  6126  wfi  6149  ordtri3or  6191  fnresdisj  6439  fnimaeq0  6453  resasplit  6522  fresaun  6523  fresaunres2  6524  fresaunres1  6525  f0rn0  6538  fvun2  6730  fveqressseq  6824  ressnop0  6892  fninfp  6913  fvsnun1  6921  fsnunfv  6926  fveqf1o  7037  orduniss2  7528  offres  7666  curry1  7782  curry2  7785  fpar  7794  wfrlem5  7942  smores3  7973  oacomf1o  8174  ralxpmap  8443  difsnen  8582  domunsncan  8600  domunsn  8651  limensuci  8677  phplem2  8681  pssnn  8720  dif1en  8735  domunfican  8775  marypha1lem  8881  zfregfr  9052  epfrs  9157  zfregs2  9159  djuin  9331  tskwe  9363  dif1card  9421  dfac8b  9442  ac10ct  9445  kmlem11  9571  kmlem12  9572  djucomen  9588  onadju  9604  ackbij1lem14  9644  ackbij1lem16  9646  ackbij1lem18  9648  fin23lem26  9736  fin23lem19  9747  fin23lem30  9753  isf32lem4  9767  isf34lem7  9790  isf34lem6  9791  axdc3lem4  9864  brdom7disj  9942  brdom6disj  9943  fpwwe2lem13  10053  canthp1lem1  10063  grothprim  10245  fzpreddisj  12951  fzdifsuc  12962  fseq1p1m1  12976  prinfzo0  13071  hashgval  13689  hashun3  13741  hashfun  13794  hashbclem  13806  xpcoidgend  14326  cotr2  14328  limsupgle  14826  prmreclem2  16243  setsdm  16509  setsfun  16510  setsfun0  16511  setsid  16530  ressinbas  16552  wunress  16556  mreexexlem2d  16908  mreexexlem4d  16910  oppcinv  17042  cnvps  17814  pmtrmvd  18576  lsmmod2  18794  lsmdisj3  18801  lsmdisjr  18802  lsmdisj2r  18803  lsmdisj3r  18804  lsmdisj2a  18805  lsmdisj2b  18806  lsmdisj3a  18807  lsmdisj3b  18808  subgdisj2  18810  pj2f  18816  pj1id  18817  frgpuplem  18890  gsummptfzsplitl  19046  dprd2da  19157  dmdprdsplit2lem  19160  dmdprdsplit2  19161  pgpfaclem1  19196  lmhmlsp  19814  pwssplit1  19824  cnfldfun  20103  psgndiflemB  20289  pjpm  20397  islindf4  20527  ltbwe  20712  psrbag0  20733  elcls  21678  mretopd  21697  restin  21771  restcld  21777  neitr  21785  resstopn  21791  lecldbas  21824  nrmsep  21962  regsep2  21981  isreg2  21982  ordthaus  21989  cmpsublem  22004  cmpsub  22005  hauscmplem  22011  bwth  22015  iunconn  22033  cldllycmp  22100  kgentopon  22143  llycmpkgen2  22155  1stckgen  22159  txkgen  22257  kqcldsat  22338  regr1lem2  22345  fbun  22445  fin1aufil  22537  fclsfnflim  22632  ustexsym  22821  restutopopn  22844  ustuqtop5  22851  ressuss  22869  metreslem  22969  blcld  23112  ressxms  23132  ressms  23133  restmetu  23177  reconn  23433  metdseq0  23459  metnrmlem3  23466  unmbl  24141  volun  24149  volinun  24150  iundisj2  24153  icombl  24168  ioombl  24169  uniioombllem2  24187  uniioombllem4  24190  dyaddisjlem  24199  dyaddisj  24200  mbfconstlem  24231  mbfeqalem2  24246  ismbf3d  24258  itg1addlem5  24304  itgsplitioo  24441  lhop  24619  tdeglem4  24661  vieta1lem2  24907  xrlimcnp  25554  perfectlem2  25814  rplogsum  26111  perpcom  26507  vtxdgoddnumeven  27343  ex-dif  28208  ococi  29188  orthin  29229  lediri  29320  pjoml2i  29368  pjoml4i  29370  cmcmlem  29374  cmbr3i  29383  cmm2i  29390  cm0  29392  fh1  29401  fh2  29402  cm2j  29403  qlaxr3i  29419  pjclem2  29979  stm1ri  30027  golem1  30054  dmdbr5  30091  mddmd2  30092  cvmdi  30107  mdsldmd1i  30114  csmdsymi  30117  mdexchi  30118  cvexchi  30152  atssma  30161  atomli  30165  atoml2i  30166  atordi  30167  atcvatlem  30168  chirredlem1  30173  chirredlem2  30174  chirredlem3  30175  atcvat4i  30180  atabsi  30184  mdsymlem1  30186  dmdbr6ati  30206  cdj3lem3  30221  disjdifr  30283  inin  30286  difeq  30289  difuncomp  30317  disjdifprg  30338  iundisj2f  30353  disjunsn  30357  imadifxp  30364  fnresin  30385  fnunres2  30441  mptprop  30458  df1stres  30463  df2ndres  30464  padct  30481  iocinif  30530  difioo  30531  fzodif1  30542  iundisj2fi  30546  xrge00  30720  symgcom  30777  tocycfvres1  30802  tocycfvres2  30803  cycpmfvlem  30804  cycpmfv3  30807  cycpmcl  30808  cycpm2tr  30811  cycpmco2f1  30816  xrge0slmod  30968  lindsun  31109  fldexttr  31136  lmxrge0  31305  esumrnmpt2  31437  esumpfinvallem  31443  ldgenpisyslem1  31532  ldgenpisys  31535  measxun2  31579  measunl  31585  carsgclctunlem1  31685  carsgclctunlem2  31687  eulerpartlemt  31739  eulerpartgbij  31740  probmeasb  31798  bayesth  31807  ballotlemfp1  31859  ballotlemfval0  31863  signstres  31955  hashreprin  32001  reprfz1  32005  chtvalz  32010  breprexpnat  32015  f1resrcmplf1d  32470  f1resfz0f1d  32471  subfacp1lem3  32542  subfacp1lem5  32544  pconnconn  32591  cvmscld  32633  cvmsss2  32634  satef  32776  satefvfmla0  32778  mrsubvrs  32882  mthmpps  32942  frpoind  33193  frind  33198  fprlem1  33250  frrlem15  33255  nosupbnd2lem1  33328  noetalem2  33331  noetalem3  33332  cldbnd  33787  bj-inrab3  34371  bj-2upln1upl  34460  bj-sscon  34465  bj-rest0  34508  bj-0int  34516  bj-ismooredr2  34525  icoreclin  34774  fin2so  35044  ptrest  35056  poimirlem3  35060  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem18  35075  poimirlem19  35076  poimirlem21  35078  poimirlem22  35079  poimirlem27  35084  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  cnambfre  35105  asindmre  35140  dvasin  35141  dvreasin  35143  dvreacos  35144  sstotbnd2  35212  bndss  35224  ineqcom  35664  inres2  35666  redundss3  36023  l1cvat  36351  pmod2iN  37145  pmodN  37146  pmodl42N  37147  osumcllem3N  37254  osumcllem4N  37255  dihmeetlem19N  38621  dihmeetALTN  38623  metakunt18  39367  elrfi  39635  diophrw  39700  eldioph2lem1  39701  eldioph2lem2  39702  diophin  39713  diophren  39754  dnwech  39992  fnwe2lem2  39995  kelac1  40007  kelac2lem  40008  kelac2  40009  lmhmlnmsplit  40031  pwssplit4  40033  pwfi2f1o  40040  proot1hash  40144  rp-fakeuninass  40224  elcnvcnvintab  40282  relintab  40283  elcnvcnvlem  40299  conrel1d  40364  dfrcl2  40375  iunrelexp0  40403  ntrk0kbimka  40742  hashnzfz  41024  zfregs2VD  41547  iunconnlem2  41641  ssinss2d  41694  restuni4  41756  restuni6  41757  iccdifioo  42152  uzinico2  42199  sumnnodd  42272  limsupvaluz  42350  cncfuni  42528  fouriersw  42873  saliincl  42967  iundjiunlem  43098  iundjiun  43099  caragenuncllem  43151  caragendifcl  43153  isomenndlem  43169  hoidmvlelem2  43235  smflimlem1  43404  perfectALTVlem2  44240  rnghmsscmap2  44597  rnghmsubcsetclem1  44599  rnghmsubcsetc  44601  rngccat  44602  rngcid  44603  rngchomrnghmresALTV  44620  rngcifuestrc  44621  funcrngcsetc  44622  rhmsscmap2  44643  rhmsubcsetclem1  44645  rhmsubcsetc  44647  ringccat  44648  ringcid  44649  rhmsscrnghm  44650  rhmsubcrngclem1  44651  rhmsubcrngc  44653  rngcresringcat  44654  funcringcsetc  44659  rngcrescrhm  44709  rhmsubclem3  44712  rhmsubc  44714  rngcrescrhmALTV  44727  rhmsubcALTVlem3  44730  rhmsubcALTVlem4  44731