Theorem incom 4172

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3405   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3406  df-in 3921

This theorem is referenced by:  ineqcom  4173  ineqcomi  4174  ineq2  4177  sseqin2  4186  in12  4192  in32  4193  in13  4194  in31  4195  inss2  4201  sslin  4206  inss  4211  dfss7  4214  indif1  4245  indifcom  4246  indir  4249  indifdir  4258  dfsymdif3  4269  dfrab2  4283  0in  4360  disjr  4414  disjdifr  4436  difdifdir  4455  uneqdifeq  4456  disjtp2  4680  iinrab2  5034  iunin1  5036  iinin1  5043  riinn0  5047  disjprg  5103  disjxun  5105  inex2  5273  inex2g  5275  rescom  5973  resindm  6001  resdmdfsn  6002  resopab  6005  imadisj  6051  intirr  6091  djudisj  6140  imainrect  6154  dmresv  6173  resdmres  6205  coeq0  6228  dfpred3  6285  predres  6312  frpoind  6315  ordtri3or  6364  fnresdisj  6638  fnimaeq0  6651  resasplit  6730  fresaun  6731  fresaunres2  6732  fresaunres1  6733  f0rn0  6745  fvun2  6953  rescnvimafod  7045  fveqressseq  7051  ressnop0  7125  fninfp  7148  fsnunfv  7161  orduniss2  7808  offres  7962  curry1  8083  curry2  8086  fpar  8095  fprlem1  8279  smores3  8322  oacomf1o  8529  domunsncan  9041  dif1ennnALT  9222  domunfican  9272  marypha1lem  9384  zfregfr  9558  epfrs  9684  zfregs2  9686  frind  9703  frrlem15  9710  djuin  9871  tskwe  9903  dfac8b  9984  ac10ct  9987  kmlem11  10114  kmlem12  10115  djucomen  10131  onadju  10147  ackbij1lem14  10185  ackbij1lem16  10187  fin23lem26  10278  fin23lem19  10289  fin23lem30  10295  isf32lem4  10309  isf34lem7  10332  isf34lem6  10333  axdc3lem4  10406  brdom7disj  10484  brdom6disj  10485  fpwwe2lem12  10595  fzpreddisj  13534  fzdifsuc  13545  fseq1p1m1  13559  prinfzo0  13659  hashun3  14349  hashbclem  14417  hash7g  14451  xpcoidgend  14941  cotr2  14943  limsupgle  15443  prmreclem2  16888  setsdm  17140  ressinbas  17215  wunress  17219  mreexexlem2d  17606  oppcinv  17742  cnvps  18537  pmtrmvd  19386  lsmmod2  19606  lsmdisj3  19613  lsmdisjr  19614  lsmdisj2r  19615  lsmdisj3r  19616  lsmdisj2a  19617  lsmdisj2b  19618  lsmdisj3a  19619  lsmdisj3b  19620  subgdisj2  19622  pj2f  19628  pj1id  19629  frgpuplem  19702  gsummptfzsplitl  19863  dprd2da  19974  dmdprdsplit2lem  19977  dmdprdsplit2  19978  pgpfaclem1  20013  rnghmsscmap2  20538  rnghmsubcsetclem1  20540  rnghmsubcsetc  20542  rngccat  20543  rngcid  20544  rngcifuestrc  20548  funcrngcsetc  20549  rhmsscmap2  20567  rhmsubcsetclem1  20569  rhmsubcsetc  20571  ringccat  20572  ringcid  20573  rhmsscrnghm  20574  rhmsubcrngclem1  20575  rhmsubcrngc  20577  rngcresringcat  20578  funcringcsetc  20583  rngcrescrhm  20593  rhmsubclem3  20596  rhmsubc  20598  lmhmlsp  20956  psgndiflemB  21509  pjpm  21617  ltbwe  21951  psrbag0  21969  elcls  22960  mretopd  22979  restin  23053  restcld  23059  resstopn  23073  lecldbas  23106  nrmsep  23244  isreg2  23264  ordthaus  23271  cmpsublem  23286  cmpsub  23287  hauscmplem  23293  bwth  23297  iunconn  23315  cldllycmp  23382  kgentopon  23425  llycmpkgen2  23437  1stckgen  23441  txkgen  23539  kqcldsat  23620  regr1lem2  23627  fbun  23727  fin1aufil  23819  fclsfnflim  23914  ustexsym  24103  restutopopn  24126  ustuqtop5  24133  ressuss  24150  metreslem  24250  blcld  24393  ressxms  24413  ressms  24414  reconn  24717  metdseq0  24743  metnrmlem3  24750  unmbl  25438  volun  25446  iundisj2  25450  icombl  25465  ioombl  25466  uniioombllem2  25484  uniioombllem4  25487  dyaddisjlem  25496  dyaddisj  25497  mbfconstlem  25528  mbfeqalem2  25543  ismbf3d  25555  itg1addlem5  25601  itgsplitioo  25739  lhop  25921  vieta1lem2  26219  xrlimcnp  26878  perfectlem2  27141  rplogsum  27438  nosupbnd2lem1  27627  sltlpss  27819  slelss  27820  perpcom  28640  vtxdgoddnumeven  29481  ex-dif  30352  ococi  31334  orthin  31375  lediri  31466  pjoml2i  31514  pjoml4i  31516  cmcmlem  31520  cmbr3i  31529  cmm2i  31536  cm0  31538  fh1  31547  fh2  31548  cm2j  31549  qlaxr3i  31565  pjclem2  32125  stm1ri  32173  golem1  32200  dmdbr5  32237  mddmd2  32238  cvmdi  32253  mdsldmd1i  32260  csmdsymi  32263  mdexchi  32264  cvexchi  32298  atssma  32307  atomli  32311  atoml2i  32312  atordi  32313  atcvatlem  32314  chirredlem1  32319  chirredlem2  32320  chirredlem3  32321  atcvat4i  32326  atabsi  32330  mdsymlem1  32332  dmdbr6ati  32352  cdj3lem3  32367  inin  32445  difuncomp  32482  iundisj2f  32519  disjunsn  32523  imadifxp  32530  fnresin  32550  mptiffisupp  32616  mptprop  32621  df1stres  32627  df2ndres  32628  padct  32643  iocinif  32704  difioo  32705  fzodif1  32715  iundisj2fi  32720  xrge00  32953  symgcom  33040  cycpm2tr  33076  cycpmco2f1  33081  xrge0slmod  33319  ssdifidlprm  33429  oppr2idl  33457  ufdprmidl  33512  1arithufdlem4  33518  lindsun  33621  fldexttr  33654  lmxrge0  33942  esumrnmpt2  34058  esumpfinvallem  34064  ldgenpisyslem1  34153  ldgenpisys  34156  measxun2  34200  measunl  34206  carsgclctunlem1  34308  carsgclctunlem2  34310  eulerpartlemt  34362  eulerpartgbij  34363  probmeasb  34421  bayesth  34430  ballotlemfp1  34483  ballotlemfval0  34487  signstres  34566  hashreprin  34611  reprfz1  34615  chtvalz  34620  breprexpnat  34625  f1resrcmplf1d  35077  f1resfz0f1d  35101  subfacp1lem3  35169  subfacp1lem5  35171  pconnconn  35218  cvmscld  35260  cvmsss2  35261  satef  35403  satefvfmla0  35405  mrsubvrs  35509  cldbnd  36314  bj-inrab3  36917  bj-2upln1upl  37012  bj-sscon  37017  bj-rest0  37081  bj-0int  37089  bj-ismooredr2  37098  icoreclin  37345  fin2so  37601  ptrest  37613  poimirlem3  37617  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  cnambfre  37662  asindmre  37697  dvasin  37698  dvreasin  37700  dvreacos  37701  sstotbnd2  37768  bndss  37780  inres2  38234  disjressuc2  38374  redundss3  38619  l1cvat  39048  pmod2iN  39843  pmodN  39844  pmodl42N  39845  osumcllem3N  39952  osumcllem4N  39953  dihmeetlem19N  41319  dihmeetALTN  41321  readvrec2  42349  elrfi  42682  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  diophin  42760  diophren  42801  dnwech  43037  fnwe2lem2  43040  kelac2lem  43053  kelac2  43054  lmhmlnmsplit  43076  pwssplit4  43078  pwfi2f1o  43085  proot1hash  43184  naddov4  43372  rp-fakeuninass  43505  elcnvcnvintab  43571  relintab  43572  elcnvcnvlem  43588  conrel1d  43652  dfrcl2  43663  iunrelexp0  43691  ntrk0kbimka  44028  hashnzfz  44309  zfregs2VD  44830  iunconnlem2  44924  ssinss2d  45054  restuni4  45115  restuni6  45116  restsubel  45147  iccdifioo  45513  uzinico2  45559  sumnnodd  45628  limsupvaluz  45706  cncfuni  45884  fouriersw  46229  saliinclf  46324  iundjiunlem  46457  iundjiun  46458  caragenuncllem  46510  caragendifcl  46512  hoidmvlelem2  46594  smflimlem1  46769  3f1oss1  47073  perfectALTVlem2  47720  rngchomrnghmresALTV  48264  rngcrescrhmALTV  48265  rhmsubcALTVlem3  48268  rhmsubcALTVlem4  48269  resinsn  48857  resinsnALT  48858  tposrescnv  48864  opndisj  48888  restclssep  48901  seposep  48911  iscnrm3rlem3  48927  iscnrm3rlem8  48932  oppczeroo  49223