Theorem incom 4150

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 3399	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
2		dfin5 3898	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
3		dfin5 3898	. 2 ⊢ (𝐵 ∩ 𝐴) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐴}
4	1, 2, 3	3eqtr4i 2770	1 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3390   ∩ cin 3889

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-rab 3391  df-in 3897

This theorem is referenced by:  ineqcom  4151  ineqcomi  4152  ineq2  4155  in12  4170  in32  4171  in13  4172  in31  4173  inss2  4179  sslin  4184  inss  4189  indif1  4223  indifcom  4224  indir  4227  indifdir  4236  dfsymdif3  4247  dfrab2  4261  difdifdir  4432  disjtp2  4661  iunin1  5015  iinin1  5022  riinn0  5026  disjprg  5082  disjxun  5084  inex2  5256  inex2g  5258  rescom  5962  resindm  5990  resdmdfsn  5991  resopab  5994  imadisj  6040  intirr  6076  djudisj  6126  imainrect  6140  dmresv  6159  resdmres  6191  coeq0  6215  dfpred3  6271  predres  6298  frpoind  6301  ordtri3or  6350  fnresdisj  6613  fnimaeq0  6626  resasplit  6705  fresaun  6706  fresaunres2  6707  fresaunres1  6708  f0rn0  6720  fvun2  6927  rescnvimafod  7020  fveqressseq  7026  ressnop0  7101  fninfp  7123  fsnunfv  7136  orduniss2  7778  offres  7930  curry1  8048  curry2  8051  fpar  8060  fprlem1  8244  smores3  8287  oacomf1o  8494  domunsncan  9009  dif1ennnALT  9181  domunfican  9226  marypha1lem  9340  zfregfr  9519  epfrs  9646  zfregs2  9648  frind  9668  frrlem15  9675  djuin  9836  tskwe  9868  dfac8b  9947  ac10ct  9950  kmlem11  10077  kmlem12  10078  djucomen  10094  onadju  10110  ackbij1lem14  10148  ackbij1lem16  10150  fin23lem26  10241  fin23lem19  10252  fin23lem30  10258  isf32lem4  10272  isf34lem7  10295  isf34lem6  10296  axdc3lem4  10369  brdom7disj  10447  brdom6disj  10448  fpwwe2lem12  10559  fzpreddisj  13521  fzdifsuc  13532  fseq1p1m1  13546  prinfzo0  13647  hashun3  14340  hashbclem  14408  hash7g  14442  xpcoidgend  14931  cotr2  14933  limsupgle  15433  prmreclem2  16882  setsdm  17134  ressinbas  17209  wunress  17213  mreexexlem2d  17605  oppcinv  17741  cnvps  18538  pmtrmvd  19425  lsmmod2  19645  lsmdisj3  19652  lsmdisjr  19653  lsmdisj2r  19654  lsmdisj3r  19655  lsmdisj2a  19656  lsmdisj2b  19657  lsmdisj3a  19658  lsmdisj3b  19659  subgdisj2  19661  pj2f  19667  pj1id  19668  frgpuplem  19741  gsummptfzsplitl  19902  dprd2da  20013  dmdprdsplit2lem  20016  dmdprdsplit2  20017  pgpfaclem1  20052  rnghmsscmap2  20600  rnghmsubcsetclem1  20602  rnghmsubcsetc  20604  rngccat  20605  rngcid  20606  rngcifuestrc  20610  funcrngcsetc  20611  rhmsscmap2  20629  rhmsubcsetclem1  20631  rhmsubcsetc  20633  ringccat  20634  ringcid  20635  rhmsscrnghm  20636  rhmsubcrngclem1  20637  rhmsubcrngc  20639  rngcresringcat  20640  funcringcsetc  20645  rngcrescrhm  20655  rhmsubclem3  20658  rhmsubc  20660  lmhmlsp  21039  psgndiflemB  21593  pjpm  21701  ltbwe  22035  psrbag0  22053  elcls  23051  mretopd  23070  restin  23144  restcld  23150  resstopn  23164  lecldbas  23197  nrmsep  23335  isreg2  23355  ordthaus  23362  cmpsublem  23377  cmpsub  23378  hauscmplem  23384  bwth  23388  iunconn  23406  cldllycmp  23473  kgentopon  23516  llycmpkgen2  23528  1stckgen  23532  txkgen  23630  kqcldsat  23711  regr1lem2  23718  fbun  23818  fin1aufil  23910  fclsfnflim  24005  ustexsym  24194  restutopopn  24216  ustuqtop5  24223  ressuss  24240  metreslem  24340  blcld  24483  ressxms  24503  ressms  24504  reconn  24807  metdseq0  24833  metnrmlem3  24840  unmbl  25517  volun  25525  iundisj2  25529  icombl  25544  ioombl  25545  uniioombllem2  25563  uniioombllem4  25566  dyaddisjlem  25575  dyaddisj  25576  mbfconstlem  25607  mbfeqalem2  25622  ismbf3d  25634  itg1addlem5  25680  itgsplitioo  25818  lhop  25996  vieta1lem2  26291  perfectlem2  27210  rplogsum  27507  nosupbnd2lem1  27696  ltslpss  27917  leslss  27918  perpcom  28798  vtxdgoddnumeven  29640  ex-dif  30511  ococi  31494  orthin  31535  lediri  31626  pjoml2i  31674  pjoml4i  31676  cmcmlem  31680  cmbr3i  31689  cmm2i  31696  cm0  31698  fh1  31707  fh2  31708  cm2j  31709  qlaxr3i  31725  pjclem2  32285  stm1ri  32333  golem1  32360  dmdbr5  32397  mddmd2  32398  cvmdi  32413  mdsldmd1i  32420  csmdsymi  32423  mdexchi  32424  cvexchi  32458  atssma  32467  atomli  32471  atoml2i  32472  atordi  32473  atcvatlem  32474  chirredlem1  32479  chirredlem2  32480  chirredlem3  32481  atcvat4i  32486  atabsi  32490  mdsymlem1  32492  dmdbr6ati  32512  cdj3lem3  32527  inin  32604  difuncomp  32641  iundisj2f  32678  disjunsn  32682  imadifxp  32689  fnresin  32715  mptiffisupp  32784  mptprop  32789  df1stres  32795  df2ndres  32796  iocinif  32872  difioo  32873  fzodif1  32883  iundisj2fi  32888  xrge00  33092  symgcom  33162  cycpm2tr  33198  cycpmco2f1  33203  xrge0slmod  33426  ssdifidlprm  33536  oppr2idl  33564  ufdprmidl  33619  1arithufdlem4  33625  psrbasfsupp  33690  lindsun  33788  fldexttr  33821  lmxrge0  34115  esumrnmpt2  34231  esumpfinvallem  34237  ldgenpisyslem1  34326  ldgenpisys  34329  measxun2  34373  measunl  34379  carsgclctunlem1  34480  carsgclctunlem2  34482  eulerpartlemt  34534  eulerpartgbij  34535  probmeasb  34593  bayesth  34602  ballotlemfp1  34655  ballotlemfval0  34659  signstres  34738  hashreprin  34783  reprfz1  34787  chtvalz  34792  breprexpnat  34797  f1resrcmplf1d  35249  f1resfz0f1d  35315  subfacp1lem3  35383  subfacp1lem5  35385  pconnconn  35432  cvmscld  35474  cvmsss2  35475  satef  35617  satefvfmla0  35619  mrsubvrs  35723  cldbnd  36527  bj-inrab3  37255  bj-2upln1upl  37350  bj-sscon  37355  bj-rest0  37424  bj-0int  37432  bj-ismooredr2  37441  icoreclin  37690  fin2so  37945  ptrest  37957  poimirlem3  37961  poimirlem11  37969  poimirlem12  37970  poimirlem13  37971  poimirlem14  37972  poimirlem15  37973  poimirlem18  37976  poimirlem21  37979  poimirlem22  37980  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  cnambfre  38006  asindmre  38041  dvasin  38042  dvreasin  38044  dvreacos  38045  sstotbnd2  38112  bndss  38124  inres2  38585  disjressuc2  38749  redundss3  39050  l1cvat  39518  pmod2iN  40312  pmodN  40313  pmodl42N  40314  osumcllem3N  40421  osumcllem4N  40422  dihmeetlem19N  41788  dihmeetALTN  41790  readvrec2  42810  elrfi  43143  diophrw  43208  eldioph2lem1  43209  eldioph2lem2  43210  diophin  43221  diophren  43262  dnwech  43497  fnwe2lem2  43500  kelac2lem  43513  kelac2  43514  lmhmlnmsplit  43536  pwssplit4  43538  pwfi2f1o  43545  proot1hash  43644  naddov4  43832  rp-fakeuninass  43964  elcnvcnvintab  44030  relintab  44031  elcnvcnvlem  44047  conrel1d  44111  dfrcl2  44122  iunrelexp0  44150  ntrk0kbimka  44487  hashnzfz  44768  zfregs2VD  45288  iunconnlem2  45382  ssinss2d  45512  restuni4  45572  restuni6  45573  restsubel  45604  iccdifioo  45966  uzinico2  46012  sumnnodd  46081  limsupvaluz  46157  cncfuni  46335  fouriersw  46680  saliinclf  46775  iundjiunlem  46908  iundjiun  46909  caragenuncllem  46961  caragendifcl  46963  hoidmvlelem2  47045  smflimlem1  47220  3f1oss1  47538  perfectALTVlem2  48213  rngchomrnghmresALTV  48770  rngcrescrhmALTV  48771  rhmsubcALTVlem3  48774  rhmsubcALTVlem4  48775  resinsn  49362  resinsnALT  49363  tposrescnv  49369  opndisj  49393  restclssep  49406  seposep  49416  iscnrm3rlem3  49432  iscnrm3rlem8  49437  oppczeroo  49727