Theorem incom 4209

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  {crab 3436   ∩ cin 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-rab 3437  df-in 3958

This theorem is referenced by:  ineqcom  4210  ineqcomi  4211  ineq2  4214  sseqin2  4223  in12  4229  in32  4230  in13  4231  in31  4232  inss2  4238  sslin  4243  inss  4248  dfss7  4251  indif1  4282  indifcom  4283  indir  4286  indifdir  4295  dfsymdif3  4306  dfrab2  4320  0in  4397  disjr  4451  disjdifr  4473  difdifdir  4492  uneqdifeq  4493  disjtp2  4716  iinrab2  5070  iunin1  5072  iinin1  5079  riinn0  5083  disjprg  5139  disjxun  5141  inex2  5318  inex2g  5320  rescom  6020  resindm  6048  resdmdfsn  6049  resopab  6052  imadisj  6098  intirr  6138  djudisj  6187  imainrect  6201  dmresv  6220  resdmres  6252  coeq0  6275  dfpred3  6332  predres  6360  frpoind  6363  wfiOLD  6372  ordtri3or  6416  fnresdisj  6688  fnimaeq0  6701  resasplit  6778  fresaun  6779  fresaunres2  6780  fresaunres1  6781  f0rn0  6793  fvun2  7001  rescnvimafod  7093  fveqressseq  7099  ressnop0  7173  fninfp  7194  fsnunfv  7207  orduniss2  7853  offres  8008  curry1  8129  curry2  8132  fpar  8141  fprlem1  8325  wfrlem5OLD  8353  smores3  8393  oacomf1o  8603  domunsncan  9112  phplem2OLD  9255  dif1ennnALT  9311  domunfican  9361  marypha1lem  9473  zfregfr  9645  epfrs  9771  zfregs2  9773  frind  9790  frrlem15  9797  djuin  9958  tskwe  9990  dfac8b  10071  ac10ct  10074  kmlem11  10201  kmlem12  10202  djucomen  10218  onadju  10234  ackbij1lem14  10272  ackbij1lem16  10274  fin23lem26  10365  fin23lem19  10376  fin23lem30  10382  isf32lem4  10396  isf34lem7  10419  isf34lem6  10420  axdc3lem4  10493  brdom7disj  10571  brdom6disj  10572  fpwwe2lem12  10682  fzpreddisj  13613  fzdifsuc  13624  fseq1p1m1  13638  prinfzo0  13738  hashun3  14423  hashbclem  14491  hash7g  14525  xpcoidgend  15014  cotr2  15016  limsupgle  15513  prmreclem2  16955  setsdm  17207  ressinbas  17291  wunress  17295  wunressOLD  17296  mreexexlem2d  17688  oppcinv  17824  cnvps  18623  pmtrmvd  19474  lsmmod2  19694  lsmdisj3  19701  lsmdisjr  19702  lsmdisj2r  19703  lsmdisj3r  19704  lsmdisj2a  19705  lsmdisj2b  19706  lsmdisj3a  19707  lsmdisj3b  19708  subgdisj2  19710  pj2f  19716  pj1id  19717  frgpuplem  19790  gsummptfzsplitl  19951  dprd2da  20062  dmdprdsplit2lem  20065  dmdprdsplit2  20066  pgpfaclem1  20101  rnghmsscmap2  20629  rnghmsubcsetclem1  20631  rnghmsubcsetc  20633  rngccat  20634  rngcid  20635  rngcifuestrc  20639  funcrngcsetc  20640  rhmsscmap2  20658  rhmsubcsetclem1  20660  rhmsubcsetc  20662  ringccat  20663  ringcid  20664  rhmsscrnghm  20665  rhmsubcrngclem1  20666  rhmsubcrngc  20668  rngcresringcat  20669  funcringcsetc  20674  rngcrescrhm  20684  rhmsubclem3  20687  rhmsubc  20689  lmhmlsp  21048  cnfldfunALTOLDOLD  21393  psgndiflemB  21618  pjpm  21728  ltbwe  22062  psrbag0  22086  elcls  23081  mretopd  23100  restin  23174  restcld  23180  resstopn  23194  lecldbas  23227  nrmsep  23365  isreg2  23385  ordthaus  23392  cmpsublem  23407  cmpsub  23408  hauscmplem  23414  bwth  23418  iunconn  23436  cldllycmp  23503  kgentopon  23546  llycmpkgen2  23558  1stckgen  23562  txkgen  23660  kqcldsat  23741  regr1lem2  23748  fbun  23848  fin1aufil  23940  fclsfnflim  24035  ustexsym  24224  restutopopn  24247  ustuqtop5  24254  ressuss  24271  metreslem  24372  blcld  24518  ressxms  24538  ressms  24539  reconn  24850  metdseq0  24876  metnrmlem3  24883  unmbl  25572  volun  25580  iundisj2  25584  icombl  25599  ioombl  25600  uniioombllem2  25618  uniioombllem4  25621  dyaddisjlem  25630  dyaddisj  25631  mbfconstlem  25662  mbfeqalem2  25677  ismbf3d  25689  itg1addlem5  25735  itgsplitioo  25873  lhop  26055  vieta1lem2  26353  xrlimcnp  27011  perfectlem2  27274  rplogsum  27571  nosupbnd2lem1  27760  sltlpss  27945  slelss  27946  perpcom  28721  vtxdgoddnumeven  29571  ex-dif  30442  ococi  31424  orthin  31465  lediri  31556  pjoml2i  31604  pjoml4i  31606  cmcmlem  31610  cmbr3i  31619  cmm2i  31626  cm0  31628  fh1  31637  fh2  31638  cm2j  31639  qlaxr3i  31655  pjclem2  32215  stm1ri  32263  golem1  32290  dmdbr5  32327  mddmd2  32328  cvmdi  32343  mdsldmd1i  32350  csmdsymi  32353  mdexchi  32354  cvexchi  32388  atssma  32397  atomli  32401  atoml2i  32402  atordi  32403  atcvatlem  32404  chirredlem1  32409  chirredlem2  32410  chirredlem3  32411  atcvat4i  32416  atabsi  32420  mdsymlem1  32422  dmdbr6ati  32442  cdj3lem3  32457  inin  32535  difuncomp  32566  iundisj2f  32603  disjunsn  32607  imadifxp  32614  fnresin  32636  mptiffisupp  32702  mptprop  32707  df1stres  32713  df2ndres  32714  padct  32731  iocinif  32783  difioo  32784  fzodif1  32794  iundisj2fi  32799  xrge00  33017  symgcom  33103  cycpm2tr  33139  cycpmco2f1  33144  xrge0slmod  33376  ssdifidlprm  33486  oppr2idl  33514  ufdprmidl  33569  1arithufdlem4  33575  lindsun  33676  fldexttr  33709  lmxrge0  33951  esumrnmpt2  34069  esumpfinvallem  34075  ldgenpisyslem1  34164  ldgenpisys  34167  measxun2  34211  measunl  34217  carsgclctunlem1  34319  carsgclctunlem2  34321  eulerpartlemt  34373  eulerpartgbij  34374  probmeasb  34432  bayesth  34441  ballotlemfp1  34494  ballotlemfval0  34498  signstres  34590  hashreprin  34635  reprfz1  34639  chtvalz  34644  breprexpnat  34649  f1resrcmplf1d  35101  f1resfz0f1d  35119  subfacp1lem3  35187  subfacp1lem5  35189  pconnconn  35236  cvmscld  35278  cvmsss2  35279  satef  35421  satefvfmla0  35423  mrsubvrs  35527  cldbnd  36327  bj-inrab3  36930  bj-2upln1upl  37025  bj-sscon  37030  bj-rest0  37094  bj-0int  37102  bj-ismooredr2  37111  icoreclin  37358  fin2so  37614  ptrest  37626  poimirlem3  37630  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  cnambfre  37675  asindmre  37710  dvasin  37711  dvreasin  37713  dvreacos  37714  sstotbnd2  37781  bndss  37793  inres2  38247  disjressuc2  38389  redundss3  38629  l1cvat  39056  pmod2iN  39851  pmodN  39852  pmodl42N  39853  osumcllem3N  39960  osumcllem4N  39961  dihmeetlem19N  41327  dihmeetALTN  41329  metakunt18  42223  readvrec2  42391  elrfi  42705  diophrw  42770  eldioph2lem1  42771  eldioph2lem2  42772  diophin  42783  diophren  42824  dnwech  43060  fnwe2lem2  43063  kelac2lem  43076  kelac2  43077  lmhmlnmsplit  43099  pwssplit4  43101  pwfi2f1o  43108  proot1hash  43207  naddov4  43396  rp-fakeuninass  43529  elcnvcnvintab  43595  relintab  43596  elcnvcnvlem  43612  conrel1d  43676  dfrcl2  43687  iunrelexp0  43715  ntrk0kbimka  44052  hashnzfz  44339  zfregs2VD  44861  iunconnlem2  44955  ssinss2d  45065  restuni4  45126  restuni6  45127  restsubel  45158  iccdifioo  45528  uzinico2  45575  sumnnodd  45645  limsupvaluz  45723  cncfuni  45901  fouriersw  46246  saliinclf  46341  iundjiunlem  46474  iundjiun  46475  caragenuncllem  46527  caragendifcl  46529  hoidmvlelem2  46611  smflimlem1  46786  3f1oss1  47087  perfectALTVlem2  47709  rngchomrnghmresALTV  48195  rngcrescrhmALTV  48196  rhmsubcALTVlem3  48199  rhmsubcALTVlem4  48200  resinsn  48772  resinsnALT  48773  tposrescnv  48779  opndisj  48800  restclssep  48813  seposep  48823  iscnrm3rlem3  48839  iscnrm3rlem8  48844