Theorem incom 4091

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3057   ∩ cin 3842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-rab 3062  df-in 3850

This theorem is referenced by:  ineqcom  4093  ineqcomi  4094  ineq2  4097  sseqin2  4106  in12  4111  in32  4112  in13  4113  in31  4114  inss2  4120  sslin  4125  inss  4129  dfss7  4131  indif1  4162  indifcom  4163  indir  4166  indifdir  4175  dfsymdif3  4187  dfrab2  4199  0in  4282  disjr  4339  disjdifr  4362  difdifdir  4378  uneqdifeq  4379  disjtp2  4607  iinrab2  4955  iunin1  4957  iinin1  4964  riinn0  4968  disjprgw  5025  disjprg  5026  disjxun  5028  inex2  5186  inex2g  5188  rescom  5851  resindm  5874  resdmdfsn  5875  resopab  5876  imadisj  5922  intirr  5952  djudisj  5999  imainrect  6013  dmresv  6032  resdmres  6064  coeq0  6088  dfpred3  6139  wfi  6162  ordtri3or  6204  fnresdisj  6456  fnimaeq0  6470  resasplit  6548  fresaun  6549  fresaunres2  6550  fresaunres1  6551  f0rn0  6563  fvun2  6760  rescnvimafod  6851  fveqressseq  6857  ressnop0  6925  fninfp  6946  fsnunfv  6959  orduniss2  7567  offres  7709  curry1  7825  curry2  7828  fpar  7837  wfrlem5  7988  smores3  8019  oacomf1o  8222  domunsncan  8666  phplem2  8747  pssnnOLD  8815  dif1enOLD  8828  domunfican  8865  marypha1lem  8970  zfregfr  9141  epfrs  9246  zfregs2  9248  djuin  9420  tskwe  9452  dfac8b  9531  ac10ct  9534  kmlem11  9660  kmlem12  9661  djucomen  9677  onadju  9693  ackbij1lem14  9733  ackbij1lem16  9735  fin23lem26  9825  fin23lem19  9836  fin23lem30  9842  isf32lem4  9856  isf34lem7  9879  isf34lem6  9880  axdc3lem4  9953  brdom7disj  10031  brdom6disj  10032  fpwwe2lem12  10142  fzpreddisj  13047  fzdifsuc  13058  fseq1p1m1  13072  prinfzo0  13167  hashun3  13837  hashbclem  13902  xpcoidgend  14424  cotr2  14426  limsupgle  14924  prmreclem2  16353  setsdm  16620  ressinbas  16663  wunress  16667  mreexexlem2d  17019  oppcinv  17155  cnvps  17938  pmtrmvd  18702  lsmmod2  18920  lsmdisj3  18927  lsmdisjr  18928  lsmdisj2r  18929  lsmdisj3r  18930  lsmdisj2a  18931  lsmdisj2b  18932  lsmdisj3a  18933  lsmdisj3b  18934  subgdisj2  18936  pj2f  18942  pj1id  18943  frgpuplem  19016  gsummptfzsplitl  19172  dprd2da  19283  dmdprdsplit2lem  19286  dmdprdsplit2  19287  pgpfaclem1  19322  lmhmlsp  19940  cnfldfun  20229  psgndiflemB  20416  pjpm  20524  ltbwe  20855  psrbag0  20874  elcls  21824  mretopd  21843  restin  21917  restcld  21923  resstopn  21937  lecldbas  21970  nrmsep  22108  isreg2  22128  ordthaus  22135  cmpsublem  22150  cmpsub  22151  hauscmplem  22157  bwth  22161  iunconn  22179  cldllycmp  22246  kgentopon  22289  llycmpkgen2  22301  1stckgen  22305  txkgen  22403  kqcldsat  22484  regr1lem2  22491  fbun  22591  fin1aufil  22683  fclsfnflim  22778  ustexsym  22967  restutopopn  22990  ustuqtop5  22997  ressuss  23015  metreslem  23115  blcld  23258  ressxms  23278  ressms  23279  reconn  23580  metdseq0  23606  metnrmlem3  23613  unmbl  24289  volun  24297  iundisj2  24301  icombl  24316  ioombl  24317  uniioombllem2  24335  uniioombllem4  24338  dyaddisjlem  24347  dyaddisj  24348  mbfconstlem  24379  mbfeqalem2  24394  ismbf3d  24406  itg1addlem5  24453  itgsplitioo  24590  lhop  24768  tdeglem4OLD  24813  vieta1lem2  25059  xrlimcnp  25706  perfectlem2  25966  rplogsum  26263  perpcom  26659  vtxdgoddnumeven  27495  ex-dif  28360  ococi  29340  orthin  29381  lediri  29472  pjoml2i  29520  pjoml4i  29522  cmcmlem  29526  cmbr3i  29535  cmm2i  29542  cm0  29544  fh1  29553  fh2  29554  cm2j  29555  qlaxr3i  29571  pjclem2  30131  stm1ri  30179  golem1  30206  dmdbr5  30243  mddmd2  30244  cvmdi  30259  mdsldmd1i  30266  csmdsymi  30269  mdexchi  30270  cvexchi  30304  atssma  30313  atomli  30317  atoml2i  30318  atordi  30319  atcvatlem  30320  chirredlem1  30325  chirredlem2  30326  chirredlem3  30327  atcvat4i  30332  atabsi  30336  mdsymlem1  30338  dmdbr6ati  30358  cdj3lem3  30373  inin  30436  difuncomp  30467  iundisj2f  30503  disjunsn  30507  imadifxp  30514  fnresin  30535  fnunres2  30590  mptprop  30606  df1stres  30611  df2ndres  30612  padct  30629  iocinif  30677  difioo  30678  fzodif1  30689  iundisj2fi  30693  xrge00  30872  symgcom  30929  cycpm2tr  30963  cycpmco2f1  30968  xrge0slmod  31120  lindsun  31278  fldexttr  31305  lmxrge0  31474  esumrnmpt2  31606  esumpfinvallem  31612  ldgenpisyslem1  31701  ldgenpisys  31704  measxun2  31748  measunl  31754  carsgclctunlem1  31854  carsgclctunlem2  31856  eulerpartlemt  31908  eulerpartgbij  31909  probmeasb  31967  bayesth  31976  ballotlemfp1  32028  ballotlemfval0  32032  signstres  32124  hashreprin  32170  reprfz1  32174  chtvalz  32179  breprexpnat  32184  f1resrcmplf1d  32630  f1resfz0f1d  32643  subfacp1lem3  32715  subfacp1lem5  32717  pconnconn  32764  cvmscld  32806  cvmsss2  32807  satef  32949  satefvfmla0  32951  mrsubvrs  33055  frpoind  33383  frind  33391  fprlem1  33455  frrlem15  33460  nosupbnd2lem1  33559  sltlpss  33725  cldbnd  34153  bj-inrab3  34748  bj-2upln1upl  34837  bj-sscon  34842  bj-rest0  34885  bj-0int  34893  bj-ismooredr2  34902  icoreclin  35151  fin2so  35387  ptrest  35399  poimirlem3  35403  poimirlem11  35411  poimirlem12  35412  poimirlem13  35413  poimirlem14  35414  poimirlem15  35415  poimirlem18  35418  poimirlem21  35421  poimirlem22  35422  mblfinlem3  35439  mblfinlem4  35440  ismblfin  35441  cnambfre  35448  asindmre  35483  dvasin  35484  dvreasin  35486  dvreacos  35487  sstotbnd2  35555  bndss  35567  inres2  36007  redundss3  36364  l1cvat  36692  pmod2iN  37486  pmodN  37487  pmodl42N  37488  osumcllem3N  37595  osumcllem4N  37596  dihmeetlem19N  38962  dihmeetALTN  38964  metakunt18  39733  elrfi  40088  diophrw  40153  eldioph2lem1  40154  eldioph2lem2  40155  diophin  40166  diophren  40207  dnwech  40445  fnwe2lem2  40448  kelac2lem  40461  kelac2  40462  lmhmlnmsplit  40484  pwssplit4  40486  pwfi2f1o  40493  proot1hash  40597  rp-fakeuninass  40677  elcnvcnvintab  40735  relintab  40736  elcnvcnvlem  40752  conrel1d  40817  dfrcl2  40828  iunrelexp0  40856  ntrk0kbimka  41195  hashnzfz  41476  zfregs2VD  41999  iunconnlem2  42093  ssinss2d  42146  restuni4  42208  restuni6  42209  iccdifioo  42593  uzinico2  42640  sumnnodd  42713  limsupvaluz  42791  cncfuni  42969  fouriersw  43314  saliincl  43408  iundjiunlem  43539  iundjiun  43540  caragenuncllem  43592  caragendifcl  43594  hoidmvlelem2  43676  smflimlem1  43845  perfectALTVlem2  44708  rnghmsscmap2  45065  rnghmsubcsetclem1  45067  rnghmsubcsetc  45069  rngccat  45070  rngcid  45071  rngchomrnghmresALTV  45088  rngcifuestrc  45089  funcrngcsetc  45090  rhmsscmap2  45111  rhmsubcsetclem1  45113  rhmsubcsetc  45115  ringccat  45116  ringcid  45117  rhmsscrnghm  45118  rhmsubcrngclem1  45119  rhmsubcrngc  45121  rngcresringcat  45122  funcringcsetc  45127  rngcrescrhm  45177  rhmsubclem3  45180  rhmsubc  45182  rngcrescrhmALTV  45195  rhmsubcALTVlem3  45198  rhmsubcALTVlem4  45199  opndisj  45718  restclssep  45731  seposep  45741  iscnrm3rlem3  45758  iscnrm3rlem8  45763