Theorem incom 4162

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  {crab 3418   ∩ cin 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-rab 3419  df-in 3913

This theorem is used by:  ineqcom  4163  ineqcomi  4164  ineq2  4167  in12  4181  in32  4182  in13  4183  in31  4184  inss2  4190  sslin  4195  inss  4201  indif1  4235  indifcom  4236  indir  4239  indifdir  4248  dfsymdif3  4259  dfrab2  4273  difdifdir  4454  disjtp2  4684  iunin1  5038  iinin1  5047  riinn0  5051  disjprg  5107  disjxun  5109  inex2  5289  inex2g  5291  rescom  6003  resindmOLD  6032  resdmdfsnOLD  6034  resopab  6038  imadisj  6084  intirr  6120  djudisj  6166  imainrect  6181  dmresv  6201  resdmres  6235  coeq0  6259  dfpred3  6317  predres  6344  frpoind  6347  ordtri3or  6397  fnresdisj  6659  fnimaeq0  6672  resasplit  6752  fresaun  6753  fresaunres2  6754  fresaunres1  6755  f0rn0  6767  fvun2  6977  rescnvimafod  7072  fveqressseq  7078  ressnop0  7156  fninfp  7178  fsnunfv  7191  f1resrcmplf1d  7278  orduniss2  7835  offres  7986  curry1  8105  curry2  8108  fpar  8117  fprlem1  8303  smores3  8346  oacomf1o  8556  domunsncan  9072  dif1ennnALT  9244  domunfican  9288  marypha1lem  9400  zfregfr  9580  epfrs  9707  zfregs2  9709  frind  9729  frrlem15  9736  djuin  9920  tskwe  9952  kmlem11  10160  kmlem12  10161  djucomen  10177  onadju  10193  ackbij1lem14  10231  ackbij1lem16  10233  fin23lem26  10324  fin23lem19  10335  fin23lem30  10341  isf32lem4  10355  isf34lem7  10378  isf34lem6  10379  axdc3lem4  10452  brdom7disj  10530  brdom6disj  10531  fpwwe2lem12  10644  fzpreddisj  13620  fzdifsuc  13631  fseq1p1m1  13645  prinfzo0  13746  f1resfz0f1d  13840  hashun3  14440  hashbclem  14509  hash7g  14543  xpcoidgend  15038  cotr2  15040  limsupgle  15554  prmreclem2  17001  setsdm  17254  ressinbas  17329  wunress  17333  mreexexlem2d  17725  oppcinv  17861  cnvps  18658  pmtrmvd  19572  lsmmod2  19792  lsmdisj3  19799  lsmdisjr  19800  lsmdisj2r  19801  lsmdisj3r  19802  lsmdisj2a  19803  lsmdisj2b  19804  lsmdisj3a  19805  lsmdisj3b  19806  subgdisj2  19808  pj2f  19814  pj1id  19815  frgpuplem  19888  gsummptfzsplitl  20049  dprd2da  20160  dmdprdsplit2lem  20163  dmdprdsplit2  20164  pgpfaclem1  20199  rnghmsscmap2  20780  rnghmsubcsetclem1  20782  rnghmsubcsetc  20784  rngccat  20785  rngcid  20786  rngcifuestrc  20790  funcrngcsetc  20791  rhmsscmap2  20809  rhmsubcsetclem1  20811  rhmsubcsetc  20813  ringccat  20814  ringcid  20815  rhmsscrnghm  20816  rhmsubcrngclem1  20817  rhmsubcrngc  20819  rngcresringcat  20820  funcringcsetc  20825  rngcrescrhm  20835  rhmsubclem3  20838  rhmsubc  20840  lmhmlsp  21222  ssdifidlprm  21538  psgndiflemB  21802  pjpm  21910  ltbwe  22247  psrbag0  22265  elcls  23282  mretopd  23301  restin  23375  restcld  23381  resstopn  23395  lecldbas  23428  nrmsep  23566  isreg2  23586  ordthaus  23593  cmpsublem  23608  cmpsub  23609  hauscmplem  23615  bwth  23619  iunconn  23637  cldllycmp  23705  kgentopon  23748  llycmpkgen2  23760  1stckgen  23764  txkgen  23862  kqcldsat  23943  regr1lem2  23950  fbun  24050  fin1aufil  24142  fclsfnflim  24237  ustexsym  24426  restutopopn  24448  ustuqtop5  24455  ressuss  24472  metreslem  24572  blcld  24715  ressxms  24735  ressms  24736  reconn  25039  metdseq0  25065  metnrmlem3  25072  unmbl  25749  volun  25757  iundisj2  25761  icombl  25776  ioombl  25777  uniioombllem2  25795  uniioombllem4  25798  dyaddisjlem  25807  dyaddisj  25808  mbfconstlem  25839  mbfeqalem2  25854  ismbf3d  25866  itg1addlem5  25912  itgsplitioo  26050  lhop  26228  vieta1lem2  26525  perfectlem2  27447  rplogsum  27744  nosupbnd2lem1  27932  ltslpss  28154  leslss  28155  perpcom  29046  prlngsym  29248  prlngpln3  29256  vtxdgoddnumeven  29963  ex-dif  30847  ococi  31830  orthin  31871  lediri  31962  pjoml2i  32010  pjoml4i  32012  cmcmlem  32016  cmbr3i  32025  cmm2i  32032  cm0  32034  fh1  32043  fh2  32044  cm2j  32045  qlaxr3i  32061  pjclem2  32621  stm1ri  32669  golem1  32696  dmdbr5  32733  mddmd2  32734  cvmdi  32749  mdsldmd1i  32756  csmdsymi  32759  mdexchi  32760  cvexchi  32794  atssma  32803  atomli  32807  atoml2i  32808  atordi  32809  atcvatlem  32810  chirredlem1  32815  chirredlem2  32816  chirredlem3  32817  atcvat4i  32822  atabsi  32826  mdsymlem1  32828  dmdbr6ati  32848  cdj3lem3  32863  inin  32935  difuncomp  32971  iundisj2f  33008  disjunsn  33012  imadifxp  33019  fnresin  33042  mptiffisupp  33111  mptprop  33116  df1stres  33122  df2ndres  33123  iocinif  33198  difioo  33199  fzodif1  33209  iundisj2fi  33214  xrge00  33400  symgcom  33469  cycpm2tr  33505  cycpmco2f1  33510  xrge0slmod  33734  oppr2idl  33834  ufdprmidl  33897  1arithufdlem4  33903  psrbasfsupp  33967  lindsun  34081  fldexttr  34114  lmxrge0  34408  esumrnmpt2  34524  esumpfinvallem  34530  ldgenpisyslem1  34620  ldgenpisys  34623  measxun2  34667  measunl  34673  carsgclctunlem1  34774  carsgclctunlem2  34776  eulerpartlemt  34828  eulerpartgbij  34829  probmeasb  34887  bayesth  34896  ballotlemfp1  34949  ballotlemfval0  34953  signstres  35029  hashreprin  35074  reprfz1  35078  chtvalz  35083  breprexpnat  35088  subfacp1lem3  35713  subfacp1lem5  35715  pconnconn  35762  cvmscld  35804  cvmsss2  35805  satef  35947  satefvfmla0  35949  mrsubvrs  36053  cldbnd  36896  bj-inrab3  37624  bj-2upln1upl  37719  bj-sscon  37724  bj-rest0  37794  bj-0int  37802  bj-ismooredr2  37811  icoreclin  38062  fin2so  38317  ptrest  38329  poimirlem3  38333  poimirlem11  38341  poimirlem12  38342  poimirlem13  38343  poimirlem14  38344  poimirlem15  38345  poimirlem18  38348  poimirlem21  38351  poimirlem22  38352  mblfinlem3  38369  mblfinlem4  38370  ismblfin  38371  cnambfre  38378  asindmre  38413  dvasin  38414  dvreasin  38416  dvreacos  38417  sstotbnd2  38485  bndss  38497  inres2  38956  disjressuc2  39120  redundss3  39421  l1cvat  39889  pmod2iN  40683  pmodN  40684  pmodl42N  40685  osumcllem3N  40792  osumcllem4N  40793  dihmeetlem19N  42159  dihmeetALTN  42161  readvrec2  43182  elrfi  43485  diophrw  43550  eldioph2lem1  43551  eldioph2lem2  43552  diophin  43563  diophren  43600  dnwech  43835  fnwe2lem2  43838  kelac2lem  43851  kelac2  43852  lmhmlnmsplit  43874  pwssplit4  43876  pwfi2f1o  43883  proot1hash  43982  naddov4  44170  rp-fakeuninass  44302  elcnvcnvintab  44368  relintab  44369  elcnvcnvlem  44385  conrel1d  44449  dfrcl2  44460  iunrelexp0  44488  ntrk0kbimka  44825  hashnzfz  45090  zfregs2VD  45609  iunconnlem2  45703  ssinss2d  45840  restuni4  45899  restuni6  45900  restsubel  45931  iccdifioo  46291  uzinico2  46337  sumnnodd  46406  cncfuni  46660  fouriersw  47005  saliinclf  47100  iundjiunlem  47233  iundjiun  47234  caragenuncllem  47286  caragendifcl  47288  hoidmvlelem2  47370  smflimlem1  47545  3f1oss1  47872  perfectALTVlem2  48547  rngchomrnghmresALTV  49103  rngcrescrhmALTV  49104  rhmsubcALTVlem3  49107  rhmsubcALTVlem4  49108  resinsn  49709  resinsnALT  49710  tposrescnv  49716  opndisj  49740  restclssep  49753  seposep  49763  iscnrm3rlem3  49779  iscnrm3rlem8  49784  oppczeroo  50074