Theorem incom 4108

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  {crab 3415   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-rab 3416  df-in 4093

This theorem is used by:  ineqcom  4109  ineqcomi  4110  ineq2  4113  in12  4127  in32  4128  in13  4129  in31  4130  inss2  4136  sslin  4141  inss  4147  indif1  4229  indifcom  4230  indir  4233  indifdir  4242  dfsymdif3  4253  dfrab2  4267  difdifdir  4449  disjtp2  4676  iunin1  5032  iinin1  5041  riinn0  5045  disjprg  5101  disjxun  5103  inex2  5281  inex2g  5283  rescom  5997  resindmOLD  6025  resdmdfsnOLD  6027  resopab  6031  imadisj  6082  intirr  6117  djudisj  6163  imainrect  6178  dmresv  6200  resdmres  6239  coeq0  6263  dfpred3  6321  predres  6348  frpoind  6351  ordtri3or  6401  fnresdisj  6667  fnimaeq0  6680  resasplit  6760  fresaun  6761  fresaunres2  6762  fresaunres1  6763  f0rn0  6775  fvun2  6985  rescnvimafod  7081  fveqressseq  7087  ressnop0  7165  fninfp  7186  fsnunfv  7199  f1resrcmplf1d  7286  orduniss2  7851  offres  8002  curry1  8125  curry2  8128  fpar  8137  fprlem1  8329  smores3  8372  oacomf1o  8584  domunsncan  9107  dif1ennnALT  9279  domunfican  9324  marypha1lem  9435  zfregfr  9615  epfrs  9742  zfregs2  9744  frind  9764  frrlem15  9771  djuin  10009  tskwe  10041  kmlem11  10249  kmlem12  10250  djucomen  10266  onadju  10282  ackbij1lem14  10320  ackbij1lem16  10322  fin23lem26  10413  fin23lem19  10424  fin23lem30  10430  isf32lem4  10444  isf34lem7  10467  isf34lem6  10468  axdc3lem4  10541  brdom7disj  10620  brdom6disj  10621  fpwwe2lem12  10737  fzpreddisj  13717  fzdifsuc  13728  fseq1p1m1  13742  prinfzo0  13843  f1resfz0f1d  13937  hashun3  14538  hashbclem  14607  hash7g  14641  xpcoidgend  15140  cotr2  15142  limsupgle  15656  prmreclem2  17107  setsdm  17360  ressinbas  17435  wunress  17439  mreexexlem2d  17831  oppcinv  17967  cnvps  18764  pmtrmvd  19682  lsmmod2  19902  lsmdisj3  19909  lsmdisjr  19910  lsmdisj2r  19911  lsmdisj3r  19912  lsmdisj2a  19913  lsmdisj2b  19914  lsmdisj3a  19915  lsmdisj3b  19916  subgdisj2  19918  pj2f  19924  pj1id  19925  frgpuplem  19998  gsummptfzsplitl  20159  dprd2da  20270  dmdprdsplit2lem  20273  dmdprdsplit2  20274  pgpfaclem1  20309  rnghmsscmap2  20893  rnghmsubcsetclem1  20895  rnghmsubcsetc  20897  rngccat  20898  rngcid  20899  rngcifuestrc  20903  funcrngcsetc  20904  rhmsscmap2  20922  rhmsubcsetclem1  20924  rhmsubcsetc  20926  ringccat  20927  ringcid  20928  rhmsscrnghm  20929  rhmsubcrngclem1  20930  rhmsubcrngc  20932  rngcresringcat  20933  funcringcsetc  20938  rngcrescrhm  20948  rhmsubclem3  20951  rhmsubc  20953  lmhmlsp  21336  ssdifidlprm  21654  psgndiflemB  21918  pjpm  22026  ltbwe  22365  psrbag0  22383  elcls  23403  mretopd  23422  restin  23496  restcld  23502  resstopn  23516  lecldbas  23549  nrmsep  23687  isreg2  23707  ordthaus  23714  cmpsublem  23729  cmpsub  23730  hauscmplem  23736  bwth  23740  iunconn  23758  cldllycmp  23826  kgentopon  23869  llycmpkgen2  23881  1stckgen  23885  txkgen  23983  kqcldsat  24064  regr1lem2  24071  fbun  24171  fin1aufil  24263  fclsfnflim  24358  ustexsym  24547  restutopopn  24569  ustuqtop5  24576  ressuss  24593  metreslem  24693  blcld  24836  ressxms  24856  ressms  24857  reconn  25160  metdseq0  25186  metnrmlem3  25193  unmbl  25870  volun  25878  iundisj2  25882  icombl  25897  ioombl  25898  uniioombllem2  25916  uniioombllem4  25919  dyaddisjlem  25928  dyaddisj  25929  mbfconstlem  25960  mbfeqalem2  25975  ismbf3d  25987  itg1addlem5  26033  itgsplitioo  26170  lhop  26348  vieta1lem2  26646  perfectlem2  27569  rplogsum  27866  nosupbnd2lem1  28084  ltslpss  28306  leslss  28307  perpcom  29200  prlngsym  29431  prlngpln3  29439  vtxdgoddnumeven  30146  ex-dif  31036  ococi  32019  orthin  32060  lediri  32151  pjoml2i  32199  pjoml4i  32201  cmcmlem  32205  cmbr3i  32214  cmm2i  32221  cm0  32223  fh1  32232  fh2  32233  cm2j  32234  qlaxr3i  32250  pjclem2  32810  stm1ri  32858  golem1  32885  dmdbr5  32922  mddmd2  32923  cvmdi  32938  mdsldmd1i  32945  csmdsymi  32948  mdexchi  32949  cvexchi  32983  atssma  32992  atomli  32996  atoml2i  32997  atordi  32998  atcvatlem  32999  chirredlem1  33004  chirredlem2  33005  chirredlem3  33006  atcvat4i  33011  atabsi  33015  mdsymlem1  33017  dmdbr6ati  33037  cdj3lem3  33052  inin  33166  difuncomp  33202  iundisj2f  33238  disjunsn  33242  imadifxp  33249  fnresin  33272  mptiffisupp  33340  mptprop  33345  df1stres  33351  df2ndres  33352  iocinif  33426  difioo  33427  fzodif1  33437  iundisj2fi  33442  xrge00  33628  symgcom  33697  cycpm2tr  33733  cycpmco2f1  33738  xrge0slmod  33962  oppr2idl  34063  ufdprmidl  34126  1arithufdlem4  34132  psrbasfsupp  34196  lindsun  34310  fldexttr  34343  lmxrge0  34637  esumrnmpt2  34753  esumpfinvallem  34759  ldgenpisyslem1  34849  ldgenpisys  34852  measxun2  34896  measunl  34902  carsgclctunlem1  35002  carsgclctunlem2  35004  eulerpartlemt  35056  eulerpartgbij  35057  probmeasb  35115  bayesth  35124  ballotlemfp1  35177  ballotlemfval0  35181  signstres  35257  hashreprin  35302  reprfz1  35306  chtvalz  35311  breprexpnat  35316  subfacp1lem3  36068  subfacp1lem5  36070  pconnconn  36117  cvmscld  36159  cvmsss2  36160  satef  36302  satefvfmla0  36304  mrsubvrs  36408  cldbnd  37241  bj-inrab3  37969  bj-2upln1upl  38064  bj-sscon  38069  bj-rest0  38153  bj-0int  38161  bj-ismooredr2  38170  icoreclin  38420  fin2so  38670  ptrest  38677  poimirlem3  38681  poimirlem11  38689  poimirlem12  38690  poimirlem13  38691  poimirlem14  38692  poimirlem15  38693  poimirlem18  38696  poimirlem21  38699  poimirlem22  38700  mblfinlem3  38717  mblfinlem4  38718  ismblfin  38719  cnambfre  38726  asindmre  38761  dvasin  38762  dvreasin  38764  dvreacos  38765  sstotbnd2  38848  bndss  38860  inres2  39319  disjressuc2  39483  redundss3  39784  l1cvat  40252  pmod2iN  41046  pmodN  41047  pmodl42N  41048  osumcllem3N  41155  osumcllem4N  41156  dihmeetlem19N  42522  dihmeetALTN  42524  readvrec2  43552  elrfi  43845  diophrw  43910  eldioph2lem1  43911  eldioph2lem2  43912  diophin  43923  diophren  43960  dnwech  44195  kelac2lem  44206  kelac2  44207  lmhmlnmsplit  44229  pwssplit4  44231  pwfi2f1o  44238  proot1hash  44337  naddov4  44525  rp-fakeuninass  44657  elcnvcnvintab  44723  relintab  44724  elcnvcnvlem  44739  conrel1d  44803  dfrcl2  44814  iunrelexp0  44842  ntrk0kbimka  45179  hashnzfz  45444  zfregs2VD  45962  iunconnlem2  46056  ssinss2d  46216  restuni4  46275  restuni6  46276  restsubel  46307  iccdifioo  46666  uzinico2  46712  sumnnodd  46781  cncfuni  47035  fouriersw  47380  saliinclf  47475  iundjiunlem  47608  iundjiun  47609  caragenuncllem  47661  caragendifcl  47663  hoidmvlelem2  47745  smflimlem1  47920  3f1oss1  48284  perfectALTVlem2  48959  rngchomrnghmresALTV  49515  rngcrescrhmALTV  49516  rhmsubcALTVlem3  49519  rhmsubcALTVlem4  49520  resinsn  50124  resinsnALT  50125  tposrescnv  50131  opndisj  50156  restclssep  50169  seposep  50179  iscnrm3rlem3  50195  iscnrm3rlem8  50200  oppczeroo  50498