Theorem incom 4155

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {crab 3413   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rab 3414  df-in 3906

This theorem is used by:  ineqcom  4156  ineqcomi  4157  ineq2  4160  in12  4174  in32  4175  in13  4176  in31  4177  inss2  4183  sslin  4188  inss  4194  indif1  4228  indifcom  4229  indir  4232  indifdir  4241  dfsymdif3  4252  dfrab2  4266  difdifdir  4447  disjtp2  4677  iunin1  5030  iinin1  5039  riinn0  5043  disjprg  5099  disjxun  5101  inex2  5278  inex2g  5280  rescom  5993  resindmOLD  6020  resdmdfsnOLD  6022  resopab  6026  imadisj  6077  intirr  6112  djudisj  6158  imainrect  6173  dmresv  6194  resdmres  6233  coeq0  6257  dfpred3  6315  predres  6342  frpoind  6345  ordtri3or  6395  fnresdisj  6659  fnimaeq0  6672  resasplit  6752  fresaun  6753  fresaunres2  6754  fresaunres1  6755  f0rn0  6767  fvun2  6977  rescnvimafod  7073  fveqressseq  7079  ressnop0  7157  fninfp  7179  fsnunfv  7192  f1resrcmplf1d  7279  orduniss2  7844  offres  7995  curry1  8115  curry2  8118  fpar  8127  fprlem1  8318  smores3  8361  oacomf1o  8573  domunsncan  9096  dif1ennnALT  9268  domunfican  9313  marypha1lem  9425  zfregfr  9605  epfrs  9732  zfregs2  9734  frind  9754  frrlem15  9761  djuin  9999  tskwe  10031  kmlem11  10239  kmlem12  10240  djucomen  10256  onadju  10272  ackbij1lem14  10310  ackbij1lem16  10312  fin23lem26  10403  fin23lem19  10414  fin23lem30  10420  isf32lem4  10434  isf34lem7  10457  isf34lem6  10458  axdc3lem4  10531  brdom7disj  10610  brdom6disj  10611  fpwwe2lem12  10727  fzpreddisj  13707  fzdifsuc  13718  fseq1p1m1  13732  prinfzo0  13833  f1resfz0f1d  13927  hashun3  14528  hashbclem  14597  hash7g  14631  xpcoidgend  15128  cotr2  15130  limsupgle  15644  prmreclem2  17095  setsdm  17348  ressinbas  17423  wunress  17427  mreexexlem2d  17819  oppcinv  17955  cnvps  18752  pmtrmvd  19670  lsmmod2  19890  lsmdisj3  19897  lsmdisjr  19898  lsmdisj2r  19899  lsmdisj3r  19900  lsmdisj2a  19901  lsmdisj2b  19902  lsmdisj3a  19903  lsmdisj3b  19904  subgdisj2  19906  pj2f  19912  pj1id  19913  frgpuplem  19986  gsummptfzsplitl  20147  dprd2da  20258  dmdprdsplit2lem  20261  dmdprdsplit2  20262  pgpfaclem1  20297  rnghmsscmap2  20881  rnghmsubcsetclem1  20883  rnghmsubcsetc  20885  rngccat  20886  rngcid  20887  rngcifuestrc  20891  funcrngcsetc  20892  rhmsscmap2  20910  rhmsubcsetclem1  20912  rhmsubcsetc  20914  ringccat  20915  ringcid  20916  rhmsscrnghm  20917  rhmsubcrngclem1  20918  rhmsubcrngc  20920  rngcresringcat  20921  funcringcsetc  20926  rngcrescrhm  20936  rhmsubclem3  20939  rhmsubc  20941  lmhmlsp  21324  ssdifidlprm  21642  psgndiflemB  21906  pjpm  22014  ltbwe  22353  psrbag0  22371  elcls  23391  mretopd  23410  restin  23484  restcld  23490  resstopn  23504  lecldbas  23537  nrmsep  23675  isreg2  23695  ordthaus  23702  cmpsublem  23717  cmpsub  23718  hauscmplem  23724  bwth  23728  iunconn  23746  cldllycmp  23814  kgentopon  23857  llycmpkgen2  23869  1stckgen  23873  txkgen  23971  kqcldsat  24052  regr1lem2  24059  fbun  24159  fin1aufil  24251  fclsfnflim  24346  ustexsym  24535  restutopopn  24557  ustuqtop5  24564  ressuss  24581  metreslem  24681  blcld  24824  ressxms  24844  ressms  24845  reconn  25148  metdseq0  25174  metnrmlem3  25181  unmbl  25858  volun  25866  iundisj2  25870  icombl  25885  ioombl  25886  uniioombllem2  25904  uniioombllem4  25907  dyaddisjlem  25916  dyaddisj  25917  mbfconstlem  25948  mbfeqalem2  25963  ismbf3d  25975  itg1addlem5  26021  itgsplitioo  26158  lhop  26336  vieta1lem2  26634  perfectlem2  27557  rplogsum  27854  nosupbnd2lem1  28072  ltslpss  28294  leslss  28295  perpcom  29188  prlngsym  29419  prlngpln3  29427  vtxdgoddnumeven  30134  ex-dif  31024  ococi  32007  orthin  32048  lediri  32139  pjoml2i  32187  pjoml4i  32189  cmcmlem  32193  cmbr3i  32202  cmm2i  32209  cm0  32211  fh1  32220  fh2  32221  cm2j  32222  qlaxr3i  32238  pjclem2  32798  stm1ri  32846  golem1  32873  dmdbr5  32910  mddmd2  32911  cvmdi  32926  mdsldmd1i  32933  csmdsymi  32936  mdexchi  32937  cvexchi  32971  atssma  32980  atomli  32984  atoml2i  32985  atordi  32986  atcvatlem  32987  chirredlem1  32992  chirredlem2  32993  chirredlem3  32994  atcvat4i  32999  atabsi  33003  mdsymlem1  33005  dmdbr6ati  33025  cdj3lem3  33040  inin  33112  difuncomp  33148  iundisj2f  33184  disjunsn  33188  imadifxp  33195  fnresin  33218  mptiffisupp  33286  mptprop  33291  df1stres  33297  df2ndres  33298  iocinif  33373  difioo  33374  fzodif1  33384  iundisj2fi  33389  xrge00  33575  symgcom  33644  cycpm2tr  33680  cycpmco2f1  33685  xrge0slmod  33909  oppr2idl  34010  ufdprmidl  34073  1arithufdlem4  34079  psrbasfsupp  34143  lindsun  34257  fldexttr  34290  lmxrge0  34584  esumrnmpt2  34700  esumpfinvallem  34706  ldgenpisyslem1  34796  ldgenpisys  34799  measxun2  34843  measunl  34849  carsgclctunlem1  34949  carsgclctunlem2  34951  eulerpartlemt  35003  eulerpartgbij  35004  probmeasb  35062  bayesth  35071  ballotlemfp1  35124  ballotlemfval0  35128  signstres  35204  hashreprin  35249  reprfz1  35253  chtvalz  35258  breprexpnat  35263  subfacp1lem3  35947  subfacp1lem5  35949  pconnconn  35996  cvmscld  36038  cvmsss2  36039  satef  36181  satefvfmla0  36183  mrsubvrs  36287  cldbnd  37114  bj-inrab3  37842  bj-2upln1upl  37937  bj-sscon  37942  bj-rest0  38014  bj-0int  38022  bj-ismooredr2  38031  icoreclin  38280  fin2so  38530  ptrest  38537  poimirlem3  38541  poimirlem11  38549  poimirlem12  38550  poimirlem13  38551  poimirlem14  38552  poimirlem15  38553  poimirlem18  38556  poimirlem21  38559  poimirlem22  38560  mblfinlem3  38577  mblfinlem4  38578  ismblfin  38579  cnambfre  38586  asindmre  38621  dvasin  38622  dvreasin  38624  dvreacos  38625  sstotbnd2  38708  bndss  38720  inres2  39179  disjressuc2  39343  redundss3  39644  l1cvat  40112  pmod2iN  40906  pmodN  40907  pmodl42N  40908  osumcllem3N  41015  osumcllem4N  41016  dihmeetlem19N  42382  dihmeetALTN  42384  readvrec2  43412  elrfi  43704  diophrw  43769  eldioph2lem1  43770  eldioph2lem2  43771  diophin  43782  diophren  43819  dnwech  44054  kelac2lem  44065  kelac2  44066  lmhmlnmsplit  44088  pwssplit4  44090  pwfi2f1o  44097  proot1hash  44196  naddov4  44384  rp-fakeuninass  44516  elcnvcnvintab  44582  relintab  44583  elcnvcnvlem  44598  conrel1d  44662  dfrcl2  44673  iunrelexp0  44701  ntrk0kbimka  45038  hashnzfz  45303  zfregs2VD  45822  iunconnlem2  45916  ssinss2d  46076  restuni4  46135  restuni6  46136  restsubel  46167  iccdifioo  46526  uzinico2  46572  sumnnodd  46641  cncfuni  46895  fouriersw  47240  saliinclf  47335  iundjiunlem  47468  iundjiun  47469  caragenuncllem  47521  caragendifcl  47523  hoidmvlelem2  47605  smflimlem1  47780  3f1oss1  48144  perfectALTVlem2  48819  rngchomrnghmresALTV  49375  rngcrescrhmALTV  49376  rhmsubcALTVlem3  49379  rhmsubcALTVlem4  49380  resinsn  49979  resinsnALT  49980  tposrescnv  49986  opndisj  50010  restclssep  50023  seposep  50033  iscnrm3rlem3  50049  iscnrm3rlem8  50054  oppczeroo  50344