Theorem incom 4161

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3399   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400  df-in 3908

This theorem is referenced by:  ineqcom  4162  ineqcomi  4163  ineq2  4166  sseqin2  4175  in12  4181  in32  4182  in13  4183  in31  4184  inss2  4190  sslin  4195  inss  4200  dfss7  4203  indif1  4234  indifcom  4235  indir  4238  indifdir  4247  dfsymdif3  4258  dfrab2  4272  0in  4349  disjr  4403  disjdifr  4425  difdifdir  4444  uneqdifeq  4445  disjtp2  4673  iinrab2  5025  iunin1  5027  iinin1  5034  riinn0  5038  disjprg  5094  disjxun  5096  inex2  5263  inex2g  5265  rescom  5961  resindm  5989  resdmdfsn  5990  resopab  5993  imadisj  6039  intirr  6075  djudisj  6125  imainrect  6139  dmresv  6158  resdmres  6190  coeq0  6214  dfpred3  6270  predres  6297  frpoind  6300  ordtri3or  6349  fnresdisj  6612  fnimaeq0  6625  resasplit  6704  fresaun  6705  fresaunres2  6706  fresaunres1  6707  f0rn0  6719  fvun2  6926  rescnvimafod  7018  fveqressseq  7024  ressnop0  7098  fninfp  7120  fsnunfv  7133  orduniss2  7775  offres  7927  curry1  8046  curry2  8049  fpar  8058  fprlem1  8242  smores3  8285  oacomf1o  8492  domunsncan  9007  dif1ennnALT  9179  domunfican  9224  marypha1lem  9338  zfregfr  9515  epfrs  9642  zfregs2  9644  frind  9664  frrlem15  9671  djuin  9832  tskwe  9864  dfac8b  9943  ac10ct  9946  kmlem11  10073  kmlem12  10074  djucomen  10090  onadju  10106  ackbij1lem14  10144  ackbij1lem16  10146  fin23lem26  10237  fin23lem19  10248  fin23lem30  10254  isf32lem4  10268  isf34lem7  10291  isf34lem6  10292  axdc3lem4  10365  brdom7disj  10443  brdom6disj  10444  fpwwe2lem12  10555  fzpreddisj  13491  fzdifsuc  13502  fseq1p1m1  13516  prinfzo0  13616  hashun3  14309  hashbclem  14377  hash7g  14411  xpcoidgend  14900  cotr2  14902  limsupgle  15402  prmreclem2  16847  setsdm  17099  ressinbas  17174  wunress  17178  mreexexlem2d  17570  oppcinv  17706  cnvps  18503  pmtrmvd  19387  lsmmod2  19607  lsmdisj3  19614  lsmdisjr  19615  lsmdisj2r  19616  lsmdisj3r  19617  lsmdisj2a  19618  lsmdisj2b  19619  lsmdisj3a  19620  lsmdisj3b  19621  subgdisj2  19623  pj2f  19629  pj1id  19630  frgpuplem  19703  gsummptfzsplitl  19864  dprd2da  19975  dmdprdsplit2lem  19978  dmdprdsplit2  19979  pgpfaclem1  20014  rnghmsscmap2  20564  rnghmsubcsetclem1  20566  rnghmsubcsetc  20568  rngccat  20569  rngcid  20570  rngcifuestrc  20574  funcrngcsetc  20575  rhmsscmap2  20593  rhmsubcsetclem1  20595  rhmsubcsetc  20597  ringccat  20598  ringcid  20599  rhmsscrnghm  20600  rhmsubcrngclem1  20601  rhmsubcrngc  20603  rngcresringcat  20604  funcringcsetc  20609  rngcrescrhm  20619  rhmsubclem3  20622  rhmsubc  20624  lmhmlsp  21003  psgndiflemB  21557  pjpm  21665  ltbwe  22001  psrbag0  22019  elcls  23019  mretopd  23038  restin  23112  restcld  23118  resstopn  23132  lecldbas  23165  nrmsep  23303  isreg2  23323  ordthaus  23330  cmpsublem  23345  cmpsub  23346  hauscmplem  23352  bwth  23356  iunconn  23374  cldllycmp  23441  kgentopon  23484  llycmpkgen2  23496  1stckgen  23500  txkgen  23598  kqcldsat  23679  regr1lem2  23686  fbun  23786  fin1aufil  23878  fclsfnflim  23973  ustexsym  24162  restutopopn  24184  ustuqtop5  24191  ressuss  24208  metreslem  24308  blcld  24451  ressxms  24471  ressms  24472  reconn  24775  metdseq0  24801  metnrmlem3  24808  unmbl  25496  volun  25504  iundisj2  25508  icombl  25523  ioombl  25524  uniioombllem2  25542  uniioombllem4  25545  dyaddisjlem  25554  dyaddisj  25555  mbfconstlem  25586  mbfeqalem2  25601  ismbf3d  25613  itg1addlem5  25659  itgsplitioo  25797  lhop  25979  vieta1lem2  26277  perfectlem2  27199  rplogsum  27496  nosupbnd2lem1  27685  ltslpss  27906  leslss  27907  perpcom  28787  vtxdgoddnumeven  29629  ex-dif  30500  ococi  31482  orthin  31523  lediri  31614  pjoml2i  31662  pjoml4i  31664  cmcmlem  31668  cmbr3i  31677  cmm2i  31684  cm0  31686  fh1  31695  fh2  31696  cm2j  31697  qlaxr3i  31713  pjclem2  32273  stm1ri  32321  golem1  32348  dmdbr5  32385  mddmd2  32386  cvmdi  32401  mdsldmd1i  32408  csmdsymi  32411  mdexchi  32412  cvexchi  32446  atssma  32455  atomli  32459  atoml2i  32460  atordi  32461  atcvatlem  32462  chirredlem1  32467  chirredlem2  32468  chirredlem3  32469  atcvat4i  32474  atabsi  32478  mdsymlem1  32480  dmdbr6ati  32500  cdj3lem3  32515  inin  32593  difuncomp  32630  iundisj2f  32667  disjunsn  32671  imadifxp  32678  fnresin  32704  mptiffisupp  32774  mptprop  32779  df1stres  32785  df2ndres  32786  padct  32799  iocinif  32863  difioo  32864  fzodif1  32874  iundisj2fi  32879  xrge00  33098  symgcom  33167  cycpm2tr  33203  cycpmco2f1  33208  xrge0slmod  33431  ssdifidlprm  33541  oppr2idl  33569  ufdprmidl  33624  1arithufdlem4  33630  psrbasfsupp  33695  lindsun  33784  fldexttr  33817  lmxrge0  34111  esumrnmpt2  34227  esumpfinvallem  34233  ldgenpisyslem1  34322  ldgenpisys  34325  measxun2  34369  measunl  34375  carsgclctunlem1  34476  carsgclctunlem2  34478  eulerpartlemt  34530  eulerpartgbij  34531  probmeasb  34589  bayesth  34598  ballotlemfp1  34651  ballotlemfval0  34655  signstres  34734  hashreprin  34779  reprfz1  34783  chtvalz  34788  breprexpnat  34793  f1resrcmplf1d  35245  f1resfz0f1d  35310  subfacp1lem3  35378  subfacp1lem5  35380  pconnconn  35427  cvmscld  35469  cvmsss2  35470  satef  35612  satefvfmla0  35614  mrsubvrs  35718  cldbnd  36522  bj-inrab3  37132  bj-2upln1upl  37227  bj-sscon  37232  bj-rest0  37300  bj-0int  37308  bj-ismooredr2  37317  icoreclin  37564  fin2so  37810  ptrest  37822  poimirlem3  37826  poimirlem11  37834  poimirlem12  37835  poimirlem13  37836  poimirlem14  37837  poimirlem15  37838  poimirlem18  37841  poimirlem21  37844  poimirlem22  37845  mblfinlem3  37862  mblfinlem4  37863  ismblfin  37864  cnambfre  37871  asindmre  37906  dvasin  37907  dvreasin  37909  dvreacos  37910  sstotbnd2  37977  bndss  37989  inres2  38446  disjressuc2  38609  redundss3  38907  l1cvat  39337  pmod2iN  40131  pmodN  40132  pmodl42N  40133  osumcllem3N  40240  osumcllem4N  40241  dihmeetlem19N  41607  dihmeetALTN  41609  readvrec2  42637  elrfi  42957  diophrw  43022  eldioph2lem1  43023  eldioph2lem2  43024  diophin  43035  diophren  43076  dnwech  43311  fnwe2lem2  43314  kelac2lem  43327  kelac2  43328  lmhmlnmsplit  43350  pwssplit4  43352  pwfi2f1o  43359  proot1hash  43458  naddov4  43646  rp-fakeuninass  43778  elcnvcnvintab  43844  relintab  43845  elcnvcnvlem  43861  conrel1d  43925  dfrcl2  43936  iunrelexp0  43964  ntrk0kbimka  44301  hashnzfz  44582  zfregs2VD  45102  iunconnlem2  45196  ssinss2d  45326  restuni4  45386  restuni6  45387  restsubel  45418  iccdifioo  45782  uzinico2  45828  sumnnodd  45897  limsupvaluz  45973  cncfuni  46151  fouriersw  46496  saliinclf  46591  iundjiunlem  46724  iundjiun  46725  caragenuncllem  46777  caragendifcl  46779  hoidmvlelem2  46861  smflimlem1  47036  3f1oss1  47342  perfectALTVlem2  47989  rngchomrnghmresALTV  48546  rngcrescrhmALTV  48547  rhmsubcALTVlem3  48550  rhmsubcALTVlem4  48551  resinsn  49138  resinsnALT  49139  tposrescnv  49145  opndisj  49169  restclssep  49182  seposep  49192  iscnrm3rlem3  49208  iscnrm3rlem8  49213  oppczeroo  49503