Theorem incom 4160

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3394   ∩ cin 3902

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3395  df-in 3910

This theorem is referenced by:  ineqcom  4161  ineqcomi  4162  ineq2  4165  sseqin2  4174  in12  4180  in32  4181  in13  4182  in31  4183  inss2  4189  sslin  4194  inss  4199  dfss7  4202  indif1  4233  indifcom  4234  indir  4237  indifdir  4246  dfsymdif3  4257  dfrab2  4271  0in  4348  disjr  4402  disjdifr  4424  difdifdir  4443  uneqdifeq  4444  disjtp2  4668  iinrab2  5019  iunin1  5021  iinin1  5028  riinn0  5032  disjprg  5088  disjxun  5090  inex2  5257  inex2g  5259  rescom  5953  resindm  5981  resdmdfsn  5982  resopab  5985  imadisj  6031  intirr  6067  djudisj  6116  imainrect  6130  dmresv  6149  resdmres  6181  coeq0  6204  dfpred3  6260  predres  6287  frpoind  6290  ordtri3or  6339  fnresdisj  6602  fnimaeq0  6615  resasplit  6694  fresaun  6695  fresaunres2  6696  fresaunres1  6697  f0rn0  6709  fvun2  6915  rescnvimafod  7007  fveqressseq  7013  ressnop0  7087  fninfp  7110  fsnunfv  7123  orduniss2  7766  offres  7918  curry1  8037  curry2  8040  fpar  8049  fprlem1  8233  smores3  8276  oacomf1o  8483  domunsncan  8994  dif1ennnALT  9166  domunfican  9211  marypha1lem  9323  zfregfr  9500  epfrs  9627  zfregs2  9629  frind  9646  frrlem15  9653  djuin  9814  tskwe  9846  dfac8b  9925  ac10ct  9928  kmlem11  10055  kmlem12  10056  djucomen  10072  onadju  10088  ackbij1lem14  10126  ackbij1lem16  10128  fin23lem26  10219  fin23lem19  10230  fin23lem30  10236  isf32lem4  10250  isf34lem7  10273  isf34lem6  10274  axdc3lem4  10347  brdom7disj  10425  brdom6disj  10426  fpwwe2lem12  10536  fzpreddisj  13476  fzdifsuc  13487  fseq1p1m1  13501  prinfzo0  13601  hashun3  14291  hashbclem  14359  hash7g  14393  xpcoidgend  14882  cotr2  14884  limsupgle  15384  prmreclem2  16829  setsdm  17081  ressinbas  17156  wunress  17160  mreexexlem2d  17551  oppcinv  17687  cnvps  18484  pmtrmvd  19335  lsmmod2  19555  lsmdisj3  19562  lsmdisjr  19563  lsmdisj2r  19564  lsmdisj3r  19565  lsmdisj2a  19566  lsmdisj2b  19567  lsmdisj3a  19568  lsmdisj3b  19569  subgdisj2  19571  pj2f  19577  pj1id  19578  frgpuplem  19651  gsummptfzsplitl  19812  dprd2da  19923  dmdprdsplit2lem  19926  dmdprdsplit2  19927  pgpfaclem1  19962  rnghmsscmap2  20514  rnghmsubcsetclem1  20516  rnghmsubcsetc  20518  rngccat  20519  rngcid  20520  rngcifuestrc  20524  funcrngcsetc  20525  rhmsscmap2  20543  rhmsubcsetclem1  20545  rhmsubcsetc  20547  ringccat  20548  ringcid  20549  rhmsscrnghm  20550  rhmsubcrngclem1  20551  rhmsubcrngc  20553  rngcresringcat  20554  funcringcsetc  20559  rngcrescrhm  20569  rhmsubclem3  20572  rhmsubc  20574  lmhmlsp  20953  psgndiflemB  21507  pjpm  21615  ltbwe  21949  psrbag0  21967  elcls  22958  mretopd  22977  restin  23051  restcld  23057  resstopn  23071  lecldbas  23104  nrmsep  23242  isreg2  23262  ordthaus  23269  cmpsublem  23284  cmpsub  23285  hauscmplem  23291  bwth  23295  iunconn  23313  cldllycmp  23380  kgentopon  23423  llycmpkgen2  23435  1stckgen  23439  txkgen  23537  kqcldsat  23618  regr1lem2  23625  fbun  23725  fin1aufil  23817  fclsfnflim  23912  ustexsym  24101  restutopopn  24124  ustuqtop5  24131  ressuss  24148  metreslem  24248  blcld  24391  ressxms  24411  ressms  24412  reconn  24715  metdseq0  24741  metnrmlem3  24748  unmbl  25436  volun  25444  iundisj2  25448  icombl  25463  ioombl  25464  uniioombllem2  25482  uniioombllem4  25485  dyaddisjlem  25494  dyaddisj  25495  mbfconstlem  25526  mbfeqalem2  25541  ismbf3d  25553  itg1addlem5  25599  itgsplitioo  25737  lhop  25919  vieta1lem2  26217  xrlimcnp  26876  perfectlem2  27139  rplogsum  27436  nosupbnd2lem1  27625  sltlpss  27822  slelss  27823  perpcom  28658  vtxdgoddnumeven  29499  ex-dif  30367  ococi  31349  orthin  31390  lediri  31481  pjoml2i  31529  pjoml4i  31531  cmcmlem  31535  cmbr3i  31544  cmm2i  31551  cm0  31553  fh1  31562  fh2  31563  cm2j  31564  qlaxr3i  31580  pjclem2  32140  stm1ri  32188  golem1  32215  dmdbr5  32252  mddmd2  32253  cvmdi  32268  mdsldmd1i  32275  csmdsymi  32278  mdexchi  32279  cvexchi  32313  atssma  32322  atomli  32326  atoml2i  32327  atordi  32328  atcvatlem  32329  chirredlem1  32334  chirredlem2  32335  chirredlem3  32336  atcvat4i  32341  atabsi  32345  mdsymlem1  32347  dmdbr6ati  32367  cdj3lem3  32382  inin  32460  difuncomp  32497  iundisj2f  32534  disjunsn  32538  imadifxp  32545  fnresin  32569  mptiffisupp  32636  mptprop  32641  df1stres  32647  df2ndres  32648  padct  32663  iocinif  32725  difioo  32726  fzodif1  32736  iundisj2fi  32741  xrge00  32969  symgcom  33026  cycpm2tr  33062  cycpmco2f1  33067  xrge0slmod  33286  ssdifidlprm  33396  oppr2idl  33424  ufdprmidl  33479  1arithufdlem4  33485  psrbasfsupp  33545  lindsun  33598  fldexttr  33631  lmxrge0  33925  esumrnmpt2  34041  esumpfinvallem  34047  ldgenpisyslem1  34136  ldgenpisys  34139  measxun2  34183  measunl  34189  carsgclctunlem1  34291  carsgclctunlem2  34293  eulerpartlemt  34345  eulerpartgbij  34346  probmeasb  34404  bayesth  34413  ballotlemfp1  34466  ballotlemfval0  34470  signstres  34549  hashreprin  34594  reprfz1  34598  chtvalz  34603  breprexpnat  34608  f1resrcmplf1d  35060  f1resfz0f1d  35097  subfacp1lem3  35165  subfacp1lem5  35167  pconnconn  35214  cvmscld  35256  cvmsss2  35257  satef  35399  satefvfmla0  35401  mrsubvrs  35505  cldbnd  36310  bj-inrab3  36913  bj-2upln1upl  37008  bj-sscon  37013  bj-rest0  37077  bj-0int  37085  bj-ismooredr2  37094  icoreclin  37341  fin2so  37597  ptrest  37609  poimirlem3  37613  poimirlem11  37621  poimirlem12  37622  poimirlem13  37623  poimirlem14  37624  poimirlem15  37625  poimirlem18  37628  poimirlem21  37631  poimirlem22  37632  mblfinlem3  37649  mblfinlem4  37650  ismblfin  37651  cnambfre  37658  asindmre  37693  dvasin  37694  dvreasin  37696  dvreacos  37697  sstotbnd2  37764  bndss  37776  inres2  38230  disjressuc2  38370  redundss3  38615  l1cvat  39044  pmod2iN  39838  pmodN  39839  pmodl42N  39840  osumcllem3N  39947  osumcllem4N  39948  dihmeetlem19N  41314  dihmeetALTN  41316  readvrec2  42344  elrfi  42677  diophrw  42742  eldioph2lem1  42743  eldioph2lem2  42744  diophin  42755  diophren  42796  dnwech  43031  fnwe2lem2  43034  kelac2lem  43047  kelac2  43048  lmhmlnmsplit  43070  pwssplit4  43072  pwfi2f1o  43079  proot1hash  43178  naddov4  43366  rp-fakeuninass  43499  elcnvcnvintab  43565  relintab  43566  elcnvcnvlem  43582  conrel1d  43646  dfrcl2  43657  iunrelexp0  43685  ntrk0kbimka  44022  hashnzfz  44303  zfregs2VD  44824  iunconnlem2  44918  ssinss2d  45048  restuni4  45109  restuni6  45110  restsubel  45141  iccdifioo  45506  uzinico2  45552  sumnnodd  45621  limsupvaluz  45699  cncfuni  45877  fouriersw  46222  saliinclf  46317  iundjiunlem  46450  iundjiun  46451  caragenuncllem  46503  caragendifcl  46505  hoidmvlelem2  46587  smflimlem1  46762  3f1oss1  47069  perfectALTVlem2  47716  rngchomrnghmresALTV  48273  rngcrescrhmALTV  48274  rhmsubcALTVlem3  48277  rhmsubcALTVlem4  48278  resinsn  48866  resinsnALT  48867  tposrescnv  48873  opndisj  48897  restclssep  48910  seposep  48920  iscnrm3rlem3  48936  iscnrm3rlem8  48941  oppczeroo  49232