Theorem incom 4163

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3401   ∩ cin 3902

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 3402  df-in 3910

This theorem is referenced by:  ineqcom  4164  ineqcomi  4165  ineq2  4168  sseqin2  4177  in12  4183  in32  4184  in13  4185  in31  4186  inss2  4192  sslin  4197  inss  4202  dfss7  4205  indif1  4236  indifcom  4237  indir  4240  indifdir  4249  dfsymdif3  4260  dfrab2  4274  0in  4351  disjr  4405  disjdifr  4427  difdifdir  4446  uneqdifeq  4447  disjtp2  4675  iinrab2  5027  iunin1  5029  iinin1  5036  riinn0  5040  disjprg  5096  disjxun  5098  inex2  5265  inex2g  5267  rescom  5969  resindm  5997  resdmdfsn  5998  resopab  6001  imadisj  6047  intirr  6083  djudisj  6133  imainrect  6147  dmresv  6166  resdmres  6198  coeq0  6222  dfpred3  6278  predres  6305  frpoind  6308  ordtri3or  6357  fnresdisj  6620  fnimaeq0  6633  resasplit  6712  fresaun  6713  fresaunres2  6714  fresaunres1  6715  f0rn0  6727  fvun2  6934  rescnvimafod  7027  fveqressseq  7033  ressnop0  7108  fninfp  7130  fsnunfv  7143  orduniss2  7785  offres  7937  curry1  8056  curry2  8059  fpar  8068  fprlem1  8252  smores3  8295  oacomf1o  8502  domunsncan  9017  dif1ennnALT  9189  domunfican  9234  marypha1lem  9348  zfregfr  9525  epfrs  9652  zfregs2  9654  frind  9674  frrlem15  9681  djuin  9842  tskwe  9874  dfac8b  9953  ac10ct  9956  kmlem11  10083  kmlem12  10084  djucomen  10100  onadju  10116  ackbij1lem14  10154  ackbij1lem16  10156  fin23lem26  10247  fin23lem19  10258  fin23lem30  10264  isf32lem4  10278  isf34lem7  10301  isf34lem6  10302  axdc3lem4  10375  brdom7disj  10453  brdom6disj  10454  fpwwe2lem12  10565  fzpreddisj  13501  fzdifsuc  13512  fseq1p1m1  13526  prinfzo0  13626  hashun3  14319  hashbclem  14387  hash7g  14421  xpcoidgend  14910  cotr2  14912  limsupgle  15412  prmreclem2  16857  setsdm  17109  ressinbas  17184  wunress  17188  mreexexlem2d  17580  oppcinv  17716  cnvps  18513  pmtrmvd  19400  lsmmod2  19620  lsmdisj3  19627  lsmdisjr  19628  lsmdisj2r  19629  lsmdisj3r  19630  lsmdisj2a  19631  lsmdisj2b  19632  lsmdisj3a  19633  lsmdisj3b  19634  subgdisj2  19636  pj2f  19642  pj1id  19643  frgpuplem  19716  gsummptfzsplitl  19877  dprd2da  19988  dmdprdsplit2lem  19991  dmdprdsplit2  19992  pgpfaclem1  20027  rnghmsscmap2  20577  rnghmsubcsetclem1  20579  rnghmsubcsetc  20581  rngccat  20582  rngcid  20583  rngcifuestrc  20587  funcrngcsetc  20588  rhmsscmap2  20606  rhmsubcsetclem1  20608  rhmsubcsetc  20610  ringccat  20611  ringcid  20612  rhmsscrnghm  20613  rhmsubcrngclem1  20614  rhmsubcrngc  20616  rngcresringcat  20617  funcringcsetc  20622  rngcrescrhm  20632  rhmsubclem3  20635  rhmsubc  20637  lmhmlsp  21016  psgndiflemB  21570  pjpm  21678  ltbwe  22014  psrbag0  22032  elcls  23032  mretopd  23051  restin  23125  restcld  23131  resstopn  23145  lecldbas  23178  nrmsep  23316  isreg2  23336  ordthaus  23343  cmpsublem  23358  cmpsub  23359  hauscmplem  23365  bwth  23369  iunconn  23387  cldllycmp  23454  kgentopon  23497  llycmpkgen2  23509  1stckgen  23513  txkgen  23611  kqcldsat  23692  regr1lem2  23699  fbun  23799  fin1aufil  23891  fclsfnflim  23986  ustexsym  24175  restutopopn  24197  ustuqtop5  24204  ressuss  24221  metreslem  24321  blcld  24464  ressxms  24484  ressms  24485  reconn  24788  metdseq0  24814  metnrmlem3  24821  unmbl  25509  volun  25517  iundisj2  25521  icombl  25536  ioombl  25537  uniioombllem2  25555  uniioombllem4  25558  dyaddisjlem  25567  dyaddisj  25568  mbfconstlem  25599  mbfeqalem2  25614  ismbf3d  25626  itg1addlem5  25672  itgsplitioo  25810  lhop  25992  vieta1lem2  26290  perfectlem2  27212  rplogsum  27509  nosupbnd2lem1  27698  ltslpss  27919  leslss  27920  perpcom  28801  vtxdgoddnumeven  29643  ex-dif  30514  ococi  31497  orthin  31538  lediri  31629  pjoml2i  31677  pjoml4i  31679  cmcmlem  31683  cmbr3i  31692  cmm2i  31699  cm0  31701  fh1  31710  fh2  31711  cm2j  31712  qlaxr3i  31728  pjclem2  32288  stm1ri  32336  golem1  32363  dmdbr5  32400  mddmd2  32401  cvmdi  32416  mdsldmd1i  32423  csmdsymi  32426  mdexchi  32427  cvexchi  32461  atssma  32470  atomli  32474  atoml2i  32475  atordi  32476  atcvatlem  32477  chirredlem1  32482  chirredlem2  32483  chirredlem3  32484  atcvat4i  32489  atabsi  32493  mdsymlem1  32495  dmdbr6ati  32515  cdj3lem3  32530  inin  32607  difuncomp  32644  iundisj2f  32681  disjunsn  32685  imadifxp  32692  fnresin  32718  mptiffisupp  32787  mptprop  32792  df1stres  32798  df2ndres  32799  iocinif  32876  difioo  32877  fzodif1  32887  iundisj2fi  32892  xrge00  33111  symgcom  33181  cycpm2tr  33217  cycpmco2f1  33222  xrge0slmod  33445  ssdifidlprm  33555  oppr2idl  33583  ufdprmidl  33638  1arithufdlem4  33644  psrbasfsupp  33709  lindsun  33807  fldexttr  33840  lmxrge0  34134  esumrnmpt2  34250  esumpfinvallem  34256  ldgenpisyslem1  34345  ldgenpisys  34348  measxun2  34392  measunl  34398  carsgclctunlem1  34499  carsgclctunlem2  34501  eulerpartlemt  34553  eulerpartgbij  34554  probmeasb  34612  bayesth  34621  ballotlemfp1  34674  ballotlemfval0  34678  signstres  34757  hashreprin  34802  reprfz1  34806  chtvalz  34811  breprexpnat  34816  f1resrcmplf1d  35268  f1resfz0f1d  35334  subfacp1lem3  35402  subfacp1lem5  35404  pconnconn  35451  cvmscld  35493  cvmsss2  35494  satef  35636  satefvfmla0  35638  mrsubvrs  35742  cldbnd  36546  bj-inrab3  37181  bj-2upln1upl  37276  bj-sscon  37281  bj-rest0  37350  bj-0int  37358  bj-ismooredr2  37367  icoreclin  37616  fin2so  37862  ptrest  37874  poimirlem3  37878  poimirlem11  37886  poimirlem12  37887  poimirlem13  37888  poimirlem14  37889  poimirlem15  37890  poimirlem18  37893  poimirlem21  37896  poimirlem22  37897  mblfinlem3  37914  mblfinlem4  37915  ismblfin  37916  cnambfre  37923  asindmre  37958  dvasin  37959  dvreasin  37961  dvreacos  37962  sstotbnd2  38029  bndss  38041  inres2  38502  disjressuc2  38666  redundss3  38967  l1cvat  39435  pmod2iN  40229  pmodN  40230  pmodl42N  40231  osumcllem3N  40338  osumcllem4N  40339  dihmeetlem19N  41705  dihmeetALTN  41707  readvrec2  42735  elrfi  43055  diophrw  43120  eldioph2lem1  43121  eldioph2lem2  43122  diophin  43133  diophren  43174  dnwech  43409  fnwe2lem2  43412  kelac2lem  43425  kelac2  43426  lmhmlnmsplit  43448  pwssplit4  43450  pwfi2f1o  43457  proot1hash  43556  naddov4  43744  rp-fakeuninass  43876  elcnvcnvintab  43942  relintab  43943  elcnvcnvlem  43959  conrel1d  44023  dfrcl2  44034  iunrelexp0  44062  ntrk0kbimka  44399  hashnzfz  44680  zfregs2VD  45200  iunconnlem2  45294  ssinss2d  45424  restuni4  45484  restuni6  45485  restsubel  45516  iccdifioo  45879  uzinico2  45925  sumnnodd  45994  limsupvaluz  46070  cncfuni  46248  fouriersw  46593  saliinclf  46688  iundjiunlem  46821  iundjiun  46822  caragenuncllem  46874  caragendifcl  46876  hoidmvlelem2  46958  smflimlem1  47133  3f1oss1  47439  perfectALTVlem2  48086  rngchomrnghmresALTV  48643  rngcrescrhmALTV  48644  rhmsubcALTVlem3  48647  rhmsubcALTVlem4  48648  resinsn  49235  resinsnALT  49236  tposrescnv  49242  opndisj  49266  restclssep  49279  seposep  49289  iscnrm3rlem3  49305  iscnrm3rlem8  49310  oppczeroo  49600