Theorem incom 4162

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

Syntax hints:   = wceq 1570   ∈ wcel 2143  {crab 3416   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-rab 3417  df-in 3912

This theorem is referenced by:  ineqcom  4163  ineqcomi  4164  ineq2  4167  in12  4181  in32  4182  in13  4183  in31  4184  inss2  4190  sslin  4195  inss  4201  indif1  4235  indifcom  4236  indir  4239  indifdir  4248  dfsymdif3  4259  dfrab2  4273  difdifdir  4452  disjtp2  4682  iunin1  5036  iinin1  5045  riinn0  5049  disjprg  5105  disjxun  5107  inex2  5287  inex2g  5289  rescom  6001  resindmOLD  6030  resdmdfsnOLD  6032  resopab  6036  imadisj  6082  intirr  6118  djudisj  6164  imainrect  6179  dmresv  6199  resdmres  6233  coeq0  6257  dfpred3  6313  predres  6340  frpoind  6343  ordtri3or  6393  fnresdisj  6655  fnimaeq0  6668  resasplit  6748  fresaun  6749  fresaunres2  6750  fresaunres1  6751  f0rn0  6763  fvun2  6973  rescnvimafod  7068  fveqressseq  7074  ressnop0  7150  fninfp  7172  fsnunfv  7185  orduniss2  7825  offres  7976  curry1  8095  curry2  8098  fpar  8107  fprlem1  8293  smores3  8336  oacomf1o  8546  domunsncan  9061  dif1ennnALT  9233  domunfican  9277  marypha1lem  9389  zfregfr  9569  epfrs  9696  zfregs2  9698  frind  9718  frrlem15  9725  djuin  9900  tskwe  9932  dfac8b  10011  ac10ct  10014  kmlem11  10140  kmlem12  10141  djucomen  10157  onadju  10173  ackbij1lem14  10211  ackbij1lem16  10213  fin23lem26  10304  fin23lem19  10315  fin23lem30  10321  isf32lem4  10335  isf34lem7  10358  isf34lem6  10359  axdc3lem4  10432  brdom7disj  10510  brdom6disj  10511  fpwwe2lem12  10622  fzpreddisj  13597  fzdifsuc  13608  fseq1p1m1  13622  prinfzo0  13723  hashun3  14416  hashbclem  14485  hash7g  14519  xpcoidgend  15008  cotr2  15010  limsupgle  15524  prmreclem2  16972  setsdm  17225  ressinbas  17300  wunress  17304  mreexexlem2d  17696  oppcinv  17832  cnvps  18629  pmtrmvd  19521  lsmmod2  19741  lsmdisj3  19748  lsmdisjr  19749  lsmdisj2r  19750  lsmdisj3r  19751  lsmdisj2a  19752  lsmdisj2b  19753  lsmdisj3a  19754  lsmdisj3b  19755  subgdisj2  19757  pj2f  19763  pj1id  19764  frgpuplem  19837  gsummptfzsplitl  19998  dprd2da  20109  dmdprdsplit2lem  20112  dmdprdsplit2  20113  pgpfaclem1  20148  rnghmsscmap2  20728  rnghmsubcsetclem1  20730  rnghmsubcsetc  20732  rngccat  20733  rngcid  20734  rngcifuestrc  20738  funcrngcsetc  20739  rhmsscmap2  20757  rhmsubcsetclem1  20759  rhmsubcsetc  20761  ringccat  20762  ringcid  20763  rhmsscrnghm  20764  rhmsubcrngclem1  20765  rhmsubcrngc  20767  rngcresringcat  20768  funcringcsetc  20773  rngcrescrhm  20783  rhmsubclem3  20786  rhmsubc  20788  lmhmlsp  21170  ssdifidlprm  21486  psgndiflemB  21750  pjpm  21858  ltbwe  22195  psrbag0  22213  elcls  23230  mretopd  23249  restin  23323  restcld  23329  resstopn  23343  lecldbas  23376  nrmsep  23514  isreg2  23534  ordthaus  23541  cmpsublem  23556  cmpsub  23557  hauscmplem  23563  bwth  23567  iunconn  23585  cldllycmp  23652  kgentopon  23695  llycmpkgen2  23707  1stckgen  23711  txkgen  23809  kqcldsat  23890  regr1lem2  23897  fbun  23997  fin1aufil  24089  fclsfnflim  24184  ustexsym  24373  restutopopn  24395  ustuqtop5  24402  ressuss  24419  metreslem  24519  blcld  24662  ressxms  24682  ressms  24683  reconn  24986  metdseq0  25012  metnrmlem3  25019  unmbl  25696  volun  25704  iundisj2  25708  icombl  25723  ioombl  25724  uniioombllem2  25742  uniioombllem4  25745  dyaddisjlem  25754  dyaddisj  25755  mbfconstlem  25786  mbfeqalem2  25801  ismbf3d  25813  itg1addlem5  25859  itgsplitioo  25997  lhop  26175  vieta1lem2  26472  perfectlem2  27394  rplogsum  27691  nosupbnd2lem1  27879  ltslpss  28101  leslss  28102  perpcom  28993  prlngsym  29191  prlngpln3  29199  vtxdgoddnumeven  29903  ex-dif  30774  ococi  31757  orthin  31798  lediri  31889  pjoml2i  31937  pjoml4i  31939  cmcmlem  31943  cmbr3i  31952  cmm2i  31959  cm0  31961  fh1  31970  fh2  31971  cm2j  31972  qlaxr3i  31988  pjclem2  32548  stm1ri  32596  golem1  32623  dmdbr5  32660  mddmd2  32661  cvmdi  32676  mdsldmd1i  32683  csmdsymi  32686  mdexchi  32687  cvexchi  32721  atssma  32730  atomli  32734  atoml2i  32735  atordi  32736  atcvatlem  32737  chirredlem1  32742  chirredlem2  32743  chirredlem3  32744  atcvat4i  32749  atabsi  32753  mdsymlem1  32755  dmdbr6ati  32775  cdj3lem3  32790  inin  32862  difuncomp  32898  iundisj2f  32935  disjunsn  32939  imadifxp  32946  fnresin  32969  mptiffisupp  33038  mptprop  33043  df1stres  33049  df2ndres  33050  iocinif  33126  difioo  33127  fzodif1  33137  iundisj2fi  33142  xrge00  33334  symgcom  33403  cycpm2tr  33439  cycpmco2f1  33444  xrge0slmod  33668  oppr2idl  33768  ufdprmidl  33831  1arithufdlem4  33837  psrbasfsupp  33901  lindsun  34015  fldexttr  34048  lmxrge0  34342  esumrnmpt2  34458  esumpfinvallem  34464  ldgenpisyslem1  34553  ldgenpisys  34556  measxun2  34600  measunl  34606  carsgclctunlem1  34707  carsgclctunlem2  34709  eulerpartlemt  34761  eulerpartgbij  34762  probmeasb  34820  bayesth  34829  ballotlemfp1  34882  ballotlemfval0  34886  signstres  34962  hashreprin  35007  reprfz1  35011  chtvalz  35016  breprexpnat  35021  f1resrcmplf1d  35475  f1resfz0f1d  35605  subfacp1lem3  35674  subfacp1lem5  35676  pconnconn  35723  cvmscld  35765  cvmsss2  35766  satef  35908  satefvfmla0  35910  mrsubvrs  36014  cldbnd  36857  bj-inrab3  37585  bj-2upln1upl  37680  bj-sscon  37685  bj-rest0  37755  bj-0int  37763  bj-ismooredr2  37772  icoreclin  38023  fin2so  38278  ptrest  38290  poimirlem3  38294  poimirlem11  38302  poimirlem12  38303  poimirlem13  38304  poimirlem14  38305  poimirlem15  38306  poimirlem18  38309  poimirlem21  38312  poimirlem22  38313  mblfinlem3  38330  mblfinlem4  38331  ismblfin  38332  cnambfre  38339  asindmre  38374  dvasin  38375  dvreasin  38377  dvreacos  38378  sstotbnd2  38445  bndss  38457  inres2  38916  disjressuc2  39080  redundss3  39381  l1cvat  39849  pmod2iN  40643  pmodN  40644  pmodl42N  40645  osumcllem3N  40752  osumcllem4N  40753  dihmeetlem19N  42119  dihmeetALTN  42121  readvrec2  43142  elrfi  43445  diophrw  43510  eldioph2lem1  43511  eldioph2lem2  43512  diophin  43523  diophren  43560  dnwech  43795  fnwe2lem2  43798  kelac2lem  43811  kelac2  43812  lmhmlnmsplit  43834  pwssplit4  43836  pwfi2f1o  43843  proot1hash  43942  naddov4  44130  rp-fakeuninass  44262  elcnvcnvintab  44328  relintab  44329  elcnvcnvlem  44345  conrel1d  44409  dfrcl2  44420  iunrelexp0  44448  ntrk0kbimka  44785  hashnzfz  45050  zfregs2VD  45569  iunconnlem2  45663  ssinss2d  45800  restuni4  45859  restuni6  45860  restsubel  45891  iccdifioo  46251  uzinico2  46297  sumnnodd  46366  cncfuni  46620  fouriersw  46965  saliinclf  47060  iundjiunlem  47193  iundjiun  47194  caragenuncllem  47246  caragendifcl  47248  hoidmvlelem2  47330  smflimlem1  47505  3f1oss1  47832  perfectALTVlem2  48507  rngchomrnghmresALTV  49064  rngcrescrhmALTV  49065  rhmsubcALTVlem3  49068  rhmsubcALTVlem4  49069  resinsn  49670  resinsnALT  49671  tposrescnv  49677  opndisj  49701  restclssep  49714  seposep  49724  iscnrm3rlem3  49740  iscnrm3rlem8  49745  oppczeroo  50035