Theorem incom 4149

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  {crab 3389   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-rab 3390  df-in 3896

This theorem is referenced by:  ineqcom  4150  ineqcomi  4151  ineq2  4154  in12  4169  in32  4170  in13  4171  in31  4172  inss2  4178  sslin  4183  inss  4188  indif1  4222  indifcom  4223  indir  4226  indifdir  4235  dfsymdif3  4246  dfrab2  4260  difdifdir  4431  disjtp2  4660  iunin1  5014  iinin1  5021  riinn0  5025  disjprg  5081  disjxun  5083  inex2  5259  inex2g  5261  rescom  5967  resindm  5995  resdmdfsn  5996  resopab  5999  imadisj  6045  intirr  6081  djudisj  6131  imainrect  6145  dmresv  6164  resdmres  6196  coeq0  6220  dfpred3  6276  predres  6303  frpoind  6306  ordtri3or  6355  fnresdisj  6618  fnimaeq0  6631  resasplit  6710  fresaun  6711  fresaunres2  6712  fresaunres1  6713  f0rn0  6725  fvun2  6932  rescnvimafod  7025  fveqressseq  7031  ressnop0  7107  fninfp  7129  fsnunfv  7142  orduniss2  7784  offres  7936  curry1  8054  curry2  8057  fpar  8066  fprlem1  8250  smores3  8293  oacomf1o  8500  domunsncan  9015  dif1ennnALT  9187  domunfican  9232  marypha1lem  9346  zfregfr  9525  epfrs  9652  zfregs2  9654  frind  9674  frrlem15  9681  djuin  9842  tskwe  9874  dfac8b  9953  ac10ct  9956  kmlem11  10083  kmlem12  10084  djucomen  10100  onadju  10116  ackbij1lem14  10154  ackbij1lem16  10156  fin23lem26  10247  fin23lem19  10258  fin23lem30  10264  isf32lem4  10278  isf34lem7  10301  isf34lem6  10302  axdc3lem4  10375  brdom7disj  10453  brdom6disj  10454  fpwwe2lem12  10565  fzpreddisj  13527  fzdifsuc  13538  fseq1p1m1  13552  prinfzo0  13653  hashun3  14346  hashbclem  14414  hash7g  14448  xpcoidgend  14937  cotr2  14939  limsupgle  15439  prmreclem2  16888  setsdm  17140  ressinbas  17215  wunress  17219  mreexexlem2d  17611  oppcinv  17747  cnvps  18544  pmtrmvd  19431  lsmmod2  19651  lsmdisj3  19658  lsmdisjr  19659  lsmdisj2r  19660  lsmdisj3r  19661  lsmdisj2a  19662  lsmdisj2b  19663  lsmdisj3a  19664  lsmdisj3b  19665  subgdisj2  19667  pj2f  19673  pj1id  19674  frgpuplem  19747  gsummptfzsplitl  19908  dprd2da  20019  dmdprdsplit2lem  20022  dmdprdsplit2  20023  pgpfaclem1  20058  rnghmsscmap2  20606  rnghmsubcsetclem1  20608  rnghmsubcsetc  20610  rngccat  20611  rngcid  20612  rngcifuestrc  20616  funcrngcsetc  20617  rhmsscmap2  20635  rhmsubcsetclem1  20637  rhmsubcsetc  20639  ringccat  20640  ringcid  20641  rhmsscrnghm  20642  rhmsubcrngclem1  20643  rhmsubcrngc  20645  rngcresringcat  20646  funcringcsetc  20651  rngcrescrhm  20661  rhmsubclem3  20664  rhmsubc  20666  lmhmlsp  21044  psgndiflemB  21580  pjpm  21688  ltbwe  22022  psrbag0  22040  elcls  23038  mretopd  23057  restin  23131  restcld  23137  resstopn  23151  lecldbas  23184  nrmsep  23322  isreg2  23342  ordthaus  23349  cmpsublem  23364  cmpsub  23365  hauscmplem  23371  bwth  23375  iunconn  23393  cldllycmp  23460  kgentopon  23503  llycmpkgen2  23515  1stckgen  23519  txkgen  23617  kqcldsat  23698  regr1lem2  23705  fbun  23805  fin1aufil  23897  fclsfnflim  23992  ustexsym  24181  restutopopn  24203  ustuqtop5  24210  ressuss  24227  metreslem  24327  blcld  24470  ressxms  24490  ressms  24491  reconn  24794  metdseq0  24820  metnrmlem3  24827  unmbl  25504  volun  25512  iundisj2  25516  icombl  25531  ioombl  25532  uniioombllem2  25550  uniioombllem4  25553  dyaddisjlem  25562  dyaddisj  25563  mbfconstlem  25594  mbfeqalem2  25609  ismbf3d  25621  itg1addlem5  25667  itgsplitioo  25805  lhop  25983  vieta1lem2  26277  perfectlem2  27193  rplogsum  27490  nosupbnd2lem1  27679  ltslpss  27900  leslss  27901  perpcom  28781  vtxdgoddnumeven  29622  ex-dif  30493  ococi  31476  orthin  31517  lediri  31608  pjoml2i  31656  pjoml4i  31658  cmcmlem  31662  cmbr3i  31671  cmm2i  31678  cm0  31680  fh1  31689  fh2  31690  cm2j  31691  qlaxr3i  31707  pjclem2  32267  stm1ri  32315  golem1  32342  dmdbr5  32379  mddmd2  32380  cvmdi  32395  mdsldmd1i  32402  csmdsymi  32405  mdexchi  32406  cvexchi  32440  atssma  32449  atomli  32453  atoml2i  32454  atordi  32455  atcvatlem  32456  chirredlem1  32461  chirredlem2  32462  chirredlem3  32463  atcvat4i  32468  atabsi  32472  mdsymlem1  32474  dmdbr6ati  32494  cdj3lem3  32509  inin  32586  difuncomp  32623  iundisj2f  32660  disjunsn  32664  imadifxp  32671  fnresin  32697  mptiffisupp  32766  mptprop  32771  df1stres  32777  df2ndres  32778  iocinif  32854  difioo  32855  fzodif1  32865  iundisj2fi  32870  xrge00  33074  symgcom  33144  cycpm2tr  33180  cycpmco2f1  33185  xrge0slmod  33408  ssdifidlprm  33518  oppr2idl  33546  ufdprmidl  33601  1arithufdlem4  33607  psrbasfsupp  33672  lindsun  33769  fldexttr  33802  lmxrge0  34096  esumrnmpt2  34212  esumpfinvallem  34218  ldgenpisyslem1  34307  ldgenpisys  34310  measxun2  34354  measunl  34360  carsgclctunlem1  34461  carsgclctunlem2  34463  eulerpartlemt  34515  eulerpartgbij  34516  probmeasb  34574  bayesth  34583  ballotlemfp1  34636  ballotlemfval0  34640  signstres  34719  hashreprin  34764  reprfz1  34768  chtvalz  34773  breprexpnat  34778  f1resrcmplf1d  35230  f1resfz0f1d  35296  subfacp1lem3  35364  subfacp1lem5  35366  pconnconn  35413  cvmscld  35455  cvmsss2  35456  satef  35598  satefvfmla0  35600  mrsubvrs  35704  cldbnd  36508  bj-inrab3  37236  bj-2upln1upl  37331  bj-sscon  37336  bj-rest0  37405  bj-0int  37413  bj-ismooredr2  37422  icoreclin  37673  fin2so  37928  ptrest  37940  poimirlem3  37944  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  cnambfre  37989  asindmre  38024  dvasin  38025  dvreasin  38027  dvreacos  38028  sstotbnd2  38095  bndss  38107  inres2  38568  disjressuc2  38732  redundss3  39033  l1cvat  39501  pmod2iN  40295  pmodN  40296  pmodl42N  40297  osumcllem3N  40404  osumcllem4N  40405  dihmeetlem19N  41771  dihmeetALTN  41773  readvrec2  42793  elrfi  43126  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  diophin  43204  diophren  43241  dnwech  43476  fnwe2lem2  43479  kelac2lem  43492  kelac2  43493  lmhmlnmsplit  43515  pwssplit4  43517  pwfi2f1o  43524  proot1hash  43623  naddov4  43811  rp-fakeuninass  43943  elcnvcnvintab  44009  relintab  44010  elcnvcnvlem  44026  conrel1d  44090  dfrcl2  44101  iunrelexp0  44129  ntrk0kbimka  44466  hashnzfz  44747  zfregs2VD  45267  iunconnlem2  45361  ssinss2d  45491  restuni4  45551  restuni6  45552  restsubel  45583  iccdifioo  45945  uzinico2  45991  sumnnodd  46060  limsupvaluz  46136  cncfuni  46314  fouriersw  46659  saliinclf  46754  iundjiunlem  46887  iundjiun  46888  caragenuncllem  46940  caragendifcl  46942  hoidmvlelem2  47024  smflimlem1  47199  3f1oss1  47523  perfectALTVlem2  48198  rngchomrnghmresALTV  48755  rngcrescrhmALTV  48756  rhmsubcALTVlem3  48759  rhmsubcALTVlem4  48760  resinsn  49347  resinsnALT  49348  tposrescnv  49354  opndisj  49378  restclssep  49391  seposep  49401  iscnrm3rlem3  49417  iscnrm3rlem8  49422  oppczeroo  49712