Theorem incom 4131

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  {crab 3067   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-rab 3072  df-in 3890

This theorem is referenced by:  ineqcom  4133  ineqcomi  4134  ineq2  4137  sseqin2  4146  in12  4151  in32  4152  in13  4153  in31  4154  inss2  4160  sslin  4165  inss  4169  dfss7  4171  indif1  4202  indifcom  4203  indir  4206  indifdir  4215  dfsymdif3  4227  dfrab2  4241  0in  4324  disjr  4380  disjdifr  4403  difdifdir  4419  uneqdifeq  4420  disjtp2  4649  iinrab2  4995  iunin1  4997  iinin1  5004  riinn0  5008  disjprgw  5065  disjprg  5066  disjxun  5068  inex2  5237  inex2g  5239  rescom  5906  resindm  5929  resdmdfsn  5930  resopab  5931  imadisj  5977  intirr  6012  djudisj  6059  imainrect  6073  dmresv  6092  resdmres  6124  coeq0  6148  dfpred3  6202  frpoind  6230  wfiOLD  6239  ordtri3or  6283  fnresdisj  6536  fnimaeq0  6550  resasplit  6628  fresaun  6629  fresaunres2  6630  fresaunres1  6631  f0rn0  6643  fvun2  6842  rescnvimafod  6933  fveqressseq  6939  ressnop0  7007  fninfp  7028  fsnunfv  7041  orduniss2  7655  offres  7799  curry1  7915  curry2  7918  fpar  7927  fprlem1  8087  wfrlem5OLD  8115  smores3  8155  oacomf1o  8358  domunsncan  8812  phplem2  8893  pssnnOLD  8969  dif1enALT  8980  domunfican  9017  marypha1lem  9122  zfregfr  9293  epfrs  9420  zfregs2  9422  frind  9439  frrlem15  9446  djuin  9607  tskwe  9639  dfac8b  9718  ac10ct  9721  kmlem11  9847  kmlem12  9848  djucomen  9864  onadju  9880  ackbij1lem14  9920  ackbij1lem16  9922  fin23lem26  10012  fin23lem19  10023  fin23lem30  10029  isf32lem4  10043  isf34lem7  10066  isf34lem6  10067  axdc3lem4  10140  brdom7disj  10218  brdom6disj  10219  fpwwe2lem12  10329  fzpreddisj  13234  fzdifsuc  13245  fseq1p1m1  13259  prinfzo0  13354  hashun3  14027  hashbclem  14092  xpcoidgend  14614  cotr2  14616  limsupgle  15114  prmreclem2  16546  setsdm  16799  ressinbas  16881  wunress  16886  wunressOLD  16887  mreexexlem2d  17271  oppcinv  17409  cnvps  18211  pmtrmvd  18979  lsmmod2  19197  lsmdisj3  19204  lsmdisjr  19205  lsmdisj2r  19206  lsmdisj3r  19207  lsmdisj2a  19208  lsmdisj2b  19209  lsmdisj3a  19210  lsmdisj3b  19211  subgdisj2  19213  pj2f  19219  pj1id  19220  frgpuplem  19293  gsummptfzsplitl  19449  dprd2da  19560  dmdprdsplit2lem  19563  dmdprdsplit2  19564  pgpfaclem1  19599  lmhmlsp  20226  cnfldfun  20522  psgndiflemB  20717  pjpm  20825  ltbwe  21155  psrbag0  21180  elcls  22132  mretopd  22151  restin  22225  restcld  22231  resstopn  22245  lecldbas  22278  nrmsep  22416  isreg2  22436  ordthaus  22443  cmpsublem  22458  cmpsub  22459  hauscmplem  22465  bwth  22469  iunconn  22487  cldllycmp  22554  kgentopon  22597  llycmpkgen2  22609  1stckgen  22613  txkgen  22711  kqcldsat  22792  regr1lem2  22799  fbun  22899  fin1aufil  22991  fclsfnflim  23086  ustexsym  23275  restutopopn  23298  ustuqtop5  23305  ressuss  23322  metreslem  23423  blcld  23567  ressxms  23587  ressms  23588  reconn  23897  metdseq0  23923  metnrmlem3  23930  unmbl  24606  volun  24614  iundisj2  24618  icombl  24633  ioombl  24634  uniioombllem2  24652  uniioombllem4  24655  dyaddisjlem  24664  dyaddisj  24665  mbfconstlem  24696  mbfeqalem2  24711  ismbf3d  24723  itg1addlem5  24770  itgsplitioo  24907  lhop  25085  tdeglem4OLD  25130  vieta1lem2  25376  xrlimcnp  26023  perfectlem2  26283  rplogsum  26580  perpcom  26978  vtxdgoddnumeven  27823  ex-dif  28688  ococi  29668  orthin  29709  lediri  29800  pjoml2i  29848  pjoml4i  29850  cmcmlem  29854  cmbr3i  29863  cmm2i  29870  cm0  29872  fh1  29881  fh2  29882  cm2j  29883  qlaxr3i  29899  pjclem2  30459  stm1ri  30507  golem1  30534  dmdbr5  30571  mddmd2  30572  cvmdi  30587  mdsldmd1i  30594  csmdsymi  30597  mdexchi  30598  cvexchi  30632  atssma  30641  atomli  30645  atoml2i  30646  atordi  30647  atcvatlem  30648  chirredlem1  30653  chirredlem2  30654  chirredlem3  30655  atcvat4i  30660  atabsi  30664  mdsymlem1  30666  dmdbr6ati  30686  cdj3lem3  30701  inin  30763  difuncomp  30794  iundisj2f  30830  disjunsn  30834  imadifxp  30841  fnresin  30862  fnunres2  30917  mptprop  30933  df1stres  30938  df2ndres  30939  padct  30956  iocinif  31004  difioo  31005  fzodif1  31016  iundisj2fi  31020  xrge00  31197  symgcom  31254  cycpm2tr  31288  cycpmco2f1  31293  xrge0slmod  31450  lindsun  31608  fldexttr  31635  lmxrge0  31804  esumrnmpt2  31936  esumpfinvallem  31942  ldgenpisyslem1  32031  ldgenpisys  32034  measxun2  32078  measunl  32084  carsgclctunlem1  32184  carsgclctunlem2  32186  eulerpartlemt  32238  eulerpartgbij  32239  probmeasb  32297  bayesth  32306  ballotlemfp1  32358  ballotlemfval0  32362  signstres  32454  hashreprin  32500  reprfz1  32504  chtvalz  32509  breprexpnat  32514  f1resrcmplf1d  32959  f1resfz0f1d  32972  subfacp1lem3  33044  subfacp1lem5  33046  pconnconn  33093  cvmscld  33135  cvmsss2  33136  satef  33278  satefvfmla0  33280  mrsubvrs  33384  nosupbnd2lem1  33845  sltlpss  34014  cldbnd  34442  bj-inrab3  35044  bj-2upln1upl  35141  bj-sscon  35146  bj-rest0  35191  bj-0int  35199  bj-ismooredr2  35208  icoreclin  35455  fin2so  35691  ptrest  35703  poimirlem3  35707  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  cnambfre  35752  asindmre  35787  dvasin  35788  dvreasin  35790  dvreacos  35791  sstotbnd2  35859  bndss  35871  inres2  36311  redundss3  36668  l1cvat  36996  pmod2iN  37790  pmodN  37791  pmodl42N  37792  osumcllem3N  37899  osumcllem4N  37900  dihmeetlem19N  39266  dihmeetALTN  39268  metakunt18  40070  elrfi  40432  diophrw  40497  eldioph2lem1  40498  eldioph2lem2  40499  diophin  40510  diophren  40551  dnwech  40789  fnwe2lem2  40792  kelac2lem  40805  kelac2  40806  lmhmlnmsplit  40828  pwssplit4  40830  pwfi2f1o  40837  proot1hash  40941  rp-fakeuninass  41021  elcnvcnvintab  41079  relintab  41080  elcnvcnvlem  41096  conrel1d  41160  dfrcl2  41171  iunrelexp0  41199  ntrk0kbimka  41538  hashnzfz  41827  zfregs2VD  42350  iunconnlem2  42444  ssinss2d  42497  restuni4  42559  restuni6  42560  iccdifioo  42943  uzinico2  42990  sumnnodd  43061  limsupvaluz  43139  cncfuni  43317  fouriersw  43662  saliincl  43756  iundjiunlem  43887  iundjiun  43888  caragenuncllem  43940  caragendifcl  43942  hoidmvlelem2  44024  smflimlem1  44193  perfectALTVlem2  45062  rnghmsscmap2  45419  rnghmsubcsetclem1  45421  rnghmsubcsetc  45423  rngccat  45424  rngcid  45425  rngchomrnghmresALTV  45442  rngcifuestrc  45443  funcrngcsetc  45444  rhmsscmap2  45465  rhmsubcsetclem1  45467  rhmsubcsetc  45469  ringccat  45470  ringcid  45471  rhmsscrnghm  45472  rhmsubcrngclem1  45473  rhmsubcrngc  45475  rngcresringcat  45476  funcringcsetc  45481  rngcrescrhm  45531  rhmsubclem3  45534  rhmsubc  45536  rngcrescrhmALTV  45549  rhmsubcALTVlem3  45552  rhmsubcALTVlem4  45553  opndisj  46084  restclssep  46097  seposep  46107  iscnrm3rlem3  46124  iscnrm3rlem8  46129