Theorem incom 4152

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

Syntax hints:   = wceq 1550   ∈ wcel 2132  {crab 3404   ∩ cin 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-rab 3405  df-in 3902

This theorem is referenced by:  ineqcom  4153  ineqcomi  4154  ineq2  4157  in12  4171  in32  4172  in13  4173  in31  4174  inss2  4180  sslin  4185  inss  4191  indif1  4225  indifcom  4226  indir  4229  indifdir  4238  dfsymdif3  4249  dfrab2  4263  difdifdir  4435  disjtp2  4665  iunin1  5019  iinin1  5026  riinn0  5030  disjprg  5086  disjxun  5088  inex2  5264  inex2g  5266  rescom  5977  resindm  6005  resdmdfsn  6006  resopab  6009  imadisj  6055  intirr  6091  djudisj  6138  imainrect  6152  dmresv  6172  resdmres  6204  coeq0  6228  dfpred3  6284  predres  6311  frpoind  6314  ordtri3or  6363  fnresdisj  6626  fnimaeq0  6639  resasplit  6719  fresaun  6720  fresaunres2  6721  fresaunres1  6722  f0rn0  6734  fvun2  6944  rescnvimafod  7039  fveqressseq  7045  ressnop0  7121  fninfp  7143  fsnunfv  7156  orduniss2  7798  offres  7949  curry1  8067  curry2  8070  fpar  8079  fprlem1  8265  smores3  8308  oacomf1o  8518  domunsncan  9034  dif1ennnALT  9206  domunfican  9251  marypha1lem  9365  zfregfr  9545  epfrs  9672  zfregs2  9674  frind  9694  frrlem15  9701  djuin  9862  tskwe  9894  dfac8b  9973  ac10ct  9976  kmlem11  10103  kmlem12  10104  djucomen  10120  onadju  10136  ackbij1lem14  10174  ackbij1lem16  10176  fin23lem26  10268  fin23lem19  10279  fin23lem30  10285  isf32lem4  10299  isf34lem7  10322  isf34lem6  10323  axdc3lem4  10396  brdom7disj  10474  brdom6disj  10475  fpwwe2lem12  10586  fzpreddisj  13564  fzdifsuc  13575  fseq1p1m1  13589  prinfzo0  13690  hashun3  14383  hashbclem  14451  hash7g  14485  xpcoidgend  14974  cotr2  14976  limsupgle  15476  prmreclem2  16925  setsdm  17178  ressinbas  17253  wunress  17257  mreexexlem2d  17649  oppcinv  17785  cnvps  18582  pmtrmvd  19468  lsmmod2  19688  lsmdisj3  19695  lsmdisjr  19696  lsmdisj2r  19697  lsmdisj3r  19698  lsmdisj2a  19699  lsmdisj2b  19700  lsmdisj3a  19701  lsmdisj3b  19702  subgdisj2  19704  pj2f  19710  pj1id  19711  frgpuplem  19784  gsummptfzsplitl  19945  dprd2da  20056  dmdprdsplit2lem  20059  dmdprdsplit2  20060  pgpfaclem1  20095  rnghmsscmap2  20647  rnghmsubcsetclem1  20649  rnghmsubcsetc  20651  rngccat  20652  rngcid  20653  rngcifuestrc  20657  funcrngcsetc  20658  rhmsscmap2  20676  rhmsubcsetclem1  20678  rhmsubcsetc  20680  ringccat  20681  ringcid  20682  rhmsscrnghm  20683  rhmsubcrngclem1  20684  rhmsubcrngc  20686  rngcresringcat  20687  funcringcsetc  20692  rngcrescrhm  20702  rhmsubclem3  20705  rhmsubc  20707  lmhmlsp  21085  psgndiflemB  21621  pjpm  21729  ltbwe  22066  psrbag0  22084  elcls  23102  mretopd  23121  restin  23195  restcld  23201  resstopn  23215  lecldbas  23248  nrmsep  23386  isreg2  23406  ordthaus  23413  cmpsublem  23428  cmpsub  23429  hauscmplem  23435  bwth  23439  iunconn  23457  cldllycmp  23524  kgentopon  23567  llycmpkgen2  23579  1stckgen  23583  txkgen  23681  kqcldsat  23762  regr1lem2  23769  fbun  23869  fin1aufil  23961  fclsfnflim  24056  ustexsym  24245  restutopopn  24267  ustuqtop5  24274  ressuss  24291  metreslem  24391  blcld  24534  ressxms  24554  ressms  24555  reconn  24858  metdseq0  24884  metnrmlem3  24891  unmbl  25568  volun  25576  iundisj2  25580  icombl  25595  ioombl  25596  uniioombllem2  25614  uniioombllem4  25617  dyaddisjlem  25626  dyaddisj  25627  mbfconstlem  25658  mbfeqalem2  25673  ismbf3d  25685  itg1addlem5  25731  itgsplitioo  25869  lhop  26047  vieta1lem2  26341  perfectlem2  27260  rplogsum  27557  nosupbnd2lem1  27745  ltslpss  27967  leslss  27968  perpcom  28848  vtxdgoddnumeven  29689  ex-dif  30560  ococi  31543  orthin  31584  lediri  31675  pjoml2i  31723  pjoml4i  31725  cmcmlem  31729  cmbr3i  31738  cmm2i  31745  cm0  31747  fh1  31756  fh2  31757  cm2j  31758  qlaxr3i  31774  pjclem2  32334  stm1ri  32382  golem1  32409  dmdbr5  32446  mddmd2  32447  cvmdi  32462  mdsldmd1i  32469  csmdsymi  32472  mdexchi  32473  cvexchi  32507  atssma  32516  atomli  32520  atoml2i  32521  atordi  32522  atcvatlem  32523  chirredlem1  32528  chirredlem2  32529  chirredlem3  32530  atcvat4i  32535  atabsi  32539  mdsymlem1  32541  dmdbr6ati  32561  cdj3lem3  32576  inin  32653  difuncomp  32691  iundisj2f  32728  disjunsn  32732  imadifxp  32739  fnresin  32765  mptiffisupp  32834  mptprop  32839  df1stres  32845  df2ndres  32846  iocinif  32922  difioo  32923  fzodif1  32933  iundisj2fi  32938  xrge00  33142  symgcom  33213  cycpm2tr  33249  cycpmco2f1  33254  xrge0slmod  33480  ssdifidlprm  33590  oppr2idl  33618  ufdprmidl  33681  1arithufdlem4  33687  psrbasfsupp  33752  lindsun  33866  fldexttr  33899  lmxrge0  34193  esumrnmpt2  34309  esumpfinvallem  34315  ldgenpisyslem1  34404  ldgenpisys  34407  measxun2  34451  measunl  34457  carsgclctunlem1  34558  carsgclctunlem2  34560  eulerpartlemt  34612  eulerpartgbij  34613  probmeasb  34671  bayesth  34680  ballotlemfp1  34733  ballotlemfval0  34737  signstres  34816  hashreprin  34861  reprfz1  34865  chtvalz  34870  breprexpnat  34875  f1resrcmplf1d  35328  f1resfz0f1d  35402  subfacp1lem3  35470  subfacp1lem5  35472  pconnconn  35519  cvmscld  35561  cvmsss2  35562  satef  35704  satefvfmla0  35706  mrsubvrs  35810  cldbnd  36624  bj-inrab3  37352  bj-2upln1upl  37447  bj-sscon  37452  bj-rest0  37521  bj-0int  37529  bj-ismooredr2  37538  icoreclin  37789  fin2so  38044  ptrest  38056  poimirlem3  38060  poimirlem11  38068  poimirlem12  38069  poimirlem13  38070  poimirlem14  38071  poimirlem15  38072  poimirlem18  38075  poimirlem21  38078  poimirlem22  38079  mblfinlem3  38096  mblfinlem4  38097  ismblfin  38098  cnambfre  38105  asindmre  38140  dvasin  38141  dvreasin  38143  dvreacos  38144  sstotbnd2  38211  bndss  38223  inres2  38684  disjressuc2  38848  redundss3  39149  l1cvat  39617  pmod2iN  40411  pmodN  40412  pmodl42N  40413  osumcllem3N  40520  osumcllem4N  40521  dihmeetlem19N  41887  dihmeetALTN  41889  readvrec2  42908  elrfi  43213  diophrw  43278  eldioph2lem1  43279  eldioph2lem2  43280  diophin  43291  diophren  43328  dnwech  43563  fnwe2lem2  43566  kelac2lem  43579  kelac2  43580  lmhmlnmsplit  43602  pwssplit4  43604  pwfi2f1o  43611  proot1hash  43710  naddov4  43898  rp-fakeuninass  44030  elcnvcnvintab  44096  relintab  44097  elcnvcnvlem  44113  conrel1d  44177  dfrcl2  44188  iunrelexp0  44216  ntrk0kbimka  44553  hashnzfz  44834  zfregs2VD  45354  iunconnlem2  45448  ssinss2d  45578  restuni4  45637  restuni6  45638  restsubel  45669  iccdifioo  46029  uzinico2  46075  sumnnodd  46144  limsupvaluz  46220  cncfuni  46398  fouriersw  46743  saliinclf  46838  iundjiunlem  46971  iundjiun  46972  caragenuncllem  47024  caragendifcl  47026  hoidmvlelem2  47108  smflimlem1  47283  3f1oss1  47607  perfectALTVlem2  48282  rngchomrnghmresALTV  48839  rngcrescrhmALTV  48840  rhmsubcALTVlem3  48843  rhmsubcALTVlem4  48844  resinsn  49431  resinsnALT  49432  tposrescnv  49438  opndisj  49462  restclssep  49475  seposep  49485  iscnrm3rlem3  49501  iscnrm3rlem8  49506  oppczeroo  49796