Theorem incom 4170

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  {crab 3423   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-rab 3424  df-in 3920

This theorem is referenced by:  ineqcom  4171  ineqcomi  4172  ineq2  4175  in12  4189  in32  4190  in13  4191  in31  4192  inss2  4198  sslin  4203  inss  4209  indif1  4243  indifcom  4244  indir  4247  indifdir  4256  dfsymdif3  4267  dfrab2  4281  difdifdir  4457  disjtp2  4687  iunin1  5040  iinin1  5049  riinn0  5053  disjprg  5109  disjxun  5111  inex2  5289  inex2g  5291  rescom  6002  resindmOLD  6031  resdmdfsnOLD  6033  resopab  6037  imadisj  6083  intirr  6119  djudisj  6165  imainrect  6180  dmresv  6200  resdmres  6234  coeq0  6258  dfpred3  6314  predres  6341  frpoind  6344  ordtri3or  6394  fnresdisj  6656  fnimaeq0  6669  resasplit  6749  fresaun  6750  fresaunres2  6751  fresaunres1  6752  f0rn0  6764  fvun2  6974  rescnvimafod  7069  fveqressseq  7075  ressnop0  7151  fninfp  7173  fsnunfv  7186  orduniss2  7829  offres  7980  curry1  8099  curry2  8102  fpar  8111  fprlem1  8297  smores3  8340  oacomf1o  8550  domunsncan  9065  dif1ennnALT  9237  domunfican  9281  marypha1lem  9393  zfregfr  9573  epfrs  9700  zfregs2  9702  frind  9722  frrlem15  9729  djuin  9904  tskwe  9936  dfac8b  10015  ac10ct  10018  kmlem11  10144  kmlem12  10145  djucomen  10161  onadju  10177  ackbij1lem14  10215  ackbij1lem16  10217  fin23lem26  10309  fin23lem19  10320  fin23lem30  10326  isf32lem4  10340  isf34lem7  10363  isf34lem6  10364  axdc3lem4  10437  brdom7disj  10515  brdom6disj  10516  fpwwe2lem12  10627  fzpreddisj  13601  fzdifsuc  13612  fseq1p1m1  13626  prinfzo0  13727  hashun3  14420  hashbclem  14489  hash7g  14523  xpcoidgend  15012  cotr2  15014  limsupgle  15528  prmreclem2  16977  setsdm  17230  ressinbas  17305  wunress  17309  mreexexlem2d  17701  oppcinv  17837  cnvps  18634  pmtrmvd  19526  lsmmod2  19746  lsmdisj3  19753  lsmdisjr  19754  lsmdisj2r  19755  lsmdisj3r  19756  lsmdisj2a  19757  lsmdisj2b  19758  lsmdisj3a  19759  lsmdisj3b  19760  subgdisj2  19762  pj2f  19768  pj1id  19769  frgpuplem  19842  gsummptfzsplitl  20003  dprd2da  20114  dmdprdsplit2lem  20117  dmdprdsplit2  20118  pgpfaclem1  20153  rnghmsscmap2  20714  rnghmsubcsetclem1  20716  rnghmsubcsetc  20718  rngccat  20719  rngcid  20720  rngcifuestrc  20724  funcrngcsetc  20725  rhmsscmap2  20743  rhmsubcsetclem1  20745  rhmsubcsetc  20747  ringccat  20748  ringcid  20749  rhmsscrnghm  20750  rhmsubcrngclem1  20751  rhmsubcrngc  20753  rngcresringcat  20754  funcringcsetc  20759  rngcrescrhm  20769  rhmsubclem3  20772  rhmsubc  20774  lmhmlsp  21148  ssdifidlprm  21455  psgndiflemB  21719  pjpm  21827  ltbwe  22164  psrbag0  22182  elcls  23199  mretopd  23218  restin  23292  restcld  23298  resstopn  23312  lecldbas  23345  nrmsep  23483  isreg2  23503  ordthaus  23510  cmpsublem  23525  cmpsub  23526  hauscmplem  23532  bwth  23536  iunconn  23554  cldllycmp  23621  kgentopon  23664  llycmpkgen2  23676  1stckgen  23680  txkgen  23778  kqcldsat  23859  regr1lem2  23866  fbun  23966  fin1aufil  24058  fclsfnflim  24153  ustexsym  24342  restutopopn  24364  ustuqtop5  24371  ressuss  24388  metreslem  24488  blcld  24631  ressxms  24651  ressms  24652  reconn  24955  metdseq0  24981  metnrmlem3  24988  unmbl  25665  volun  25673  iundisj2  25677  icombl  25692  ioombl  25693  uniioombllem2  25711  uniioombllem4  25714  dyaddisjlem  25723  dyaddisj  25724  mbfconstlem  25755  mbfeqalem2  25770  ismbf3d  25782  itg1addlem5  25828  itgsplitioo  25966  lhop  26144  vieta1lem2  26441  perfectlem2  27360  rplogsum  27657  nosupbnd2lem1  27845  ltslpss  28067  leslss  28068  perpcom  28952  prlngsym  29146  prlngpln3  29152  vtxdgoddnumeven  29844  ex-dif  30715  ococi  31698  orthin  31739  lediri  31830  pjoml2i  31878  pjoml4i  31880  cmcmlem  31884  cmbr3i  31893  cmm2i  31900  cm0  31902  fh1  31911  fh2  31912  cm2j  31913  qlaxr3i  31929  pjclem2  32489  stm1ri  32537  golem1  32564  dmdbr5  32601  mddmd2  32602  cvmdi  32617  mdsldmd1i  32624  csmdsymi  32627  mdexchi  32628  cvexchi  32662  atssma  32671  atomli  32675  atoml2i  32676  atordi  32677  atcvatlem  32678  chirredlem1  32683  chirredlem2  32684  chirredlem3  32685  atcvat4i  32690  atabsi  32694  mdsymlem1  32696  dmdbr6ati  32716  cdj3lem3  32731  inin  32803  difuncomp  32839  iundisj2f  32876  disjunsn  32880  imadifxp  32887  fnresin  32910  mptiffisupp  32979  mptprop  32984  df1stres  32990  df2ndres  32991  iocinif  33067  difioo  33068  fzodif1  33078  iundisj2fi  33083  xrge00  33275  symgcom  33344  cycpm2tr  33380  cycpmco2f1  33385  xrge0slmod  33611  oppr2idl  33713  ufdprmidl  33776  1arithufdlem4  33782  psrbasfsupp  33846  lindsun  33960  fldexttr  33993  lmxrge0  34287  esumrnmpt2  34403  esumpfinvallem  34409  ldgenpisyslem1  34498  ldgenpisys  34501  measxun2  34545  measunl  34551  carsgclctunlem1  34652  carsgclctunlem2  34654  eulerpartlemt  34706  eulerpartgbij  34707  probmeasb  34765  bayesth  34774  ballotlemfp1  34827  ballotlemfval0  34831  signstres  34907  hashreprin  34952  reprfz1  34956  chtvalz  34961  breprexpnat  34966  f1resrcmplf1d  35419  f1resfz0f1d  35538  subfacp1lem3  35607  subfacp1lem5  35609  pconnconn  35656  cvmscld  35698  cvmsss2  35699  satef  35841  satefvfmla0  35843  mrsubvrs  35947  cldbnd  36760  bj-inrab3  37487  bj-2upln1upl  37582  bj-sscon  37587  bj-rest0  37657  bj-0int  37665  bj-ismooredr2  37674  icoreclin  37925  fin2so  38180  ptrest  38192  poimirlem3  38196  poimirlem11  38204  poimirlem12  38205  poimirlem13  38206  poimirlem14  38207  poimirlem15  38208  poimirlem18  38211  poimirlem21  38214  poimirlem22  38215  mblfinlem3  38232  mblfinlem4  38233  ismblfin  38234  cnambfre  38241  asindmre  38276  dvasin  38277  dvreasin  38279  dvreacos  38280  sstotbnd2  38347  bndss  38359  inres2  38820  disjressuc2  38984  redundss3  39285  l1cvat  39753  pmod2iN  40547  pmodN  40548  pmodl42N  40549  osumcllem3N  40656  osumcllem4N  40657  dihmeetlem19N  42023  dihmeetALTN  42025  readvrec2  43046  elrfi  43351  diophrw  43416  eldioph2lem1  43417  eldioph2lem2  43418  diophin  43429  diophren  43466  dnwech  43701  fnwe2lem2  43704  kelac2lem  43717  kelac2  43718  lmhmlnmsplit  43740  pwssplit4  43742  pwfi2f1o  43749  proot1hash  43848  naddov4  44036  rp-fakeuninass  44168  elcnvcnvintab  44234  relintab  44235  elcnvcnvlem  44251  conrel1d  44315  dfrcl2  44326  iunrelexp0  44354  ntrk0kbimka  44691  hashnzfz  44956  zfregs2VD  45475  iunconnlem2  45569  ssinss2d  45706  restuni4  45765  restuni6  45766  restsubel  45797  iccdifioo  46157  uzinico2  46203  sumnnodd  46272  cncfuni  46526  fouriersw  46871  saliinclf  46966  iundjiunlem  47099  iundjiun  47100  caragenuncllem  47152  caragendifcl  47154  hoidmvlelem2  47236  smflimlem1  47411  3f1oss1  47735  perfectALTVlem2  48410  rngchomrnghmresALTV  48967  rngcrescrhmALTV  48968  rhmsubcALTVlem3  48971  rhmsubcALTVlem4  48972  resinsn  49569  resinsnALT  49570  tposrescnv  49576  opndisj  49600  restclssep  49613  seposep  49623  iscnrm3rlem3  49639  iscnrm3rlem8  49644  oppczeroo  49934