Theorem incom 4161

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

Syntax hints:   = wceq 1560   ∈ wcel 2142  {crab 3414   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-rab 3415  df-in 3911

This theorem is referenced by:  ineqcom  4162  ineqcomi  4163  ineq2  4166  in12  4180  in32  4181  in13  4182  in31  4183  inss2  4189  sslin  4194  inss  4200  indif1  4234  indifcom  4235  indir  4238  indifdir  4247  dfsymdif3  4258  dfrab2  4272  difdifdir  4445  disjtp2  4675  iunin1  5029  iinin1  5036  riinn0  5040  disjprg  5096  disjxun  5098  inex2  5274  inex2g  5276  rescom  5988  resindmOLD  6017  resdmdfsnOLD  6019  resopab  6023  imadisj  6069  intirr  6105  djudisj  6152  imainrect  6167  dmresv  6187  resdmres  6219  coeq0  6243  dfpred3  6299  predres  6326  frpoind  6329  ordtri3or  6378  fnresdisj  6641  fnimaeq0  6654  resasplit  6734  fresaun  6735  fresaunres2  6736  fresaunres1  6737  f0rn0  6749  fvun2  6959  rescnvimafod  7054  fveqressseq  7060  ressnop0  7136  fninfp  7158  fsnunfv  7171  orduniss2  7813  offres  7964  curry1  8083  curry2  8086  fpar  8095  fprlem1  8281  smores3  8324  oacomf1o  8534  domunsncan  9049  dif1ennnALT  9221  domunfican  9266  marypha1lem  9379  zfregfr  9559  epfrs  9686  zfregs2  9688  frind  9708  frrlem15  9715  djuin  9876  tskwe  9908  dfac8b  9987  ac10ct  9990  kmlem11  10117  kmlem12  10118  djucomen  10134  onadju  10150  ackbij1lem14  10188  ackbij1lem16  10190  fin23lem26  10282  fin23lem19  10293  fin23lem30  10299  isf32lem4  10313  isf34lem7  10336  isf34lem6  10337  axdc3lem4  10410  brdom7disj  10488  brdom6disj  10489  fpwwe2lem12  10600  fzpreddisj  13578  fzdifsuc  13589  fseq1p1m1  13603  prinfzo0  13704  hashun3  14397  hashbclem  14465  hash7g  14499  xpcoidgend  14988  cotr2  14990  limsupgle  15504  prmreclem2  16953  setsdm  17206  ressinbas  17281  wunress  17285  mreexexlem2d  17677  oppcinv  17813  cnvps  18610  pmtrmvd  19496  lsmmod2  19716  lsmdisj3  19723  lsmdisjr  19724  lsmdisj2r  19725  lsmdisj3r  19726  lsmdisj2a  19727  lsmdisj2b  19728  lsmdisj3a  19729  lsmdisj3b  19730  subgdisj2  19732  pj2f  19738  pj1id  19739  frgpuplem  19812  gsummptfzsplitl  19973  dprd2da  20084  dmdprdsplit2lem  20087  dmdprdsplit2  20088  pgpfaclem1  20123  rnghmsscmap2  20679  rnghmsubcsetclem1  20681  rnghmsubcsetc  20683  rngccat  20684  rngcid  20685  rngcifuestrc  20689  funcrngcsetc  20690  rhmsscmap2  20708  rhmsubcsetclem1  20710  rhmsubcsetc  20712  ringccat  20713  ringcid  20714  rhmsscrnghm  20715  rhmsubcrngclem1  20716  rhmsubcrngc  20718  rngcresringcat  20719  funcringcsetc  20724  rngcrescrhm  20734  rhmsubclem3  20737  rhmsubc  20739  lmhmlsp  21116  psgndiflemB  21652  pjpm  21760  ltbwe  22097  psrbag0  22115  elcls  23133  mretopd  23152  restin  23226  restcld  23232  resstopn  23246  lecldbas  23279  nrmsep  23417  isreg2  23437  ordthaus  23444  cmpsublem  23459  cmpsub  23460  hauscmplem  23466  bwth  23470  iunconn  23488  cldllycmp  23555  kgentopon  23598  llycmpkgen2  23610  1stckgen  23614  txkgen  23712  kqcldsat  23793  regr1lem2  23800  fbun  23900  fin1aufil  23992  fclsfnflim  24087  ustexsym  24276  restutopopn  24298  ustuqtop5  24305  ressuss  24322  metreslem  24422  blcld  24565  ressxms  24585  ressms  24586  reconn  24889  metdseq0  24915  metnrmlem3  24922  unmbl  25599  volun  25607  iundisj2  25611  icombl  25626  ioombl  25627  uniioombllem2  25645  uniioombllem4  25648  dyaddisjlem  25657  dyaddisj  25658  mbfconstlem  25689  mbfeqalem2  25704  ismbf3d  25716  itg1addlem5  25762  itgsplitioo  25900  lhop  26078  vieta1lem2  26375  perfectlem2  27294  rplogsum  27591  nosupbnd2lem1  27779  ltslpss  28001  leslss  28002  perpcom  28886  prlngsym  29068  vtxdgoddnumeven  29754  ex-dif  30625  ococi  31608  orthin  31649  lediri  31740  pjoml2i  31788  pjoml4i  31790  cmcmlem  31794  cmbr3i  31803  cmm2i  31810  cm0  31812  fh1  31821  fh2  31822  cm2j  31823  qlaxr3i  31839  pjclem2  32399  stm1ri  32447  golem1  32474  dmdbr5  32511  mddmd2  32512  cvmdi  32527  mdsldmd1i  32534  csmdsymi  32537  mdexchi  32538  cvexchi  32572  atssma  32581  atomli  32585  atoml2i  32586  atordi  32587  atcvatlem  32588  chirredlem1  32593  chirredlem2  32594  chirredlem3  32595  atcvat4i  32600  atabsi  32604  mdsymlem1  32606  dmdbr6ati  32626  cdj3lem3  32641  inin  32715  difuncomp  32753  iundisj2f  32790  disjunsn  32794  imadifxp  32801  fnresin  32826  mptiffisupp  32895  mptprop  32900  df1stres  32906  df2ndres  32907  iocinif  32983  difioo  32984  fzodif1  32994  iundisj2fi  32999  xrge00  33192  symgcom  33263  cycpm2tr  33299  cycpmco2f1  33304  xrge0slmod  33534  ssdifidlprm  33645  oppr2idl  33674  ufdprmidl  33737  1arithufdlem4  33743  psrbasfsupp  33808  lindsun  33922  fldexttr  33955  lmxrge0  34249  esumrnmpt2  34365  esumpfinvallem  34371  ldgenpisyslem1  34460  ldgenpisys  34463  measxun2  34507  measunl  34513  carsgclctunlem1  34614  carsgclctunlem2  34616  eulerpartlemt  34668  eulerpartgbij  34669  probmeasb  34727  bayesth  34736  ballotlemfp1  34789  ballotlemfval0  34793  signstres  34869  hashreprin  34914  reprfz1  34918  chtvalz  34923  breprexpnat  34928  f1resrcmplf1d  35381  f1resfz0f1d  35464  subfacp1lem3  35532  subfacp1lem5  35534  pconnconn  35581  cvmscld  35623  cvmsss2  35624  satef  35766  satefvfmla0  35768  mrsubvrs  35872  cldbnd  36686  bj-inrab3  37414  bj-2upln1upl  37509  bj-sscon  37514  bj-rest0  37583  bj-0int  37591  bj-ismooredr2  37600  icoreclin  37851  fin2so  38106  ptrest  38118  poimirlem3  38122  poimirlem11  38130  poimirlem12  38131  poimirlem13  38132  poimirlem14  38133  poimirlem15  38134  poimirlem18  38137  poimirlem21  38140  poimirlem22  38141  mblfinlem3  38158  mblfinlem4  38159  ismblfin  38160  cnambfre  38167  asindmre  38202  dvasin  38203  dvreasin  38205  dvreacos  38206  sstotbnd2  38273  bndss  38285  inres2  38746  disjressuc2  38910  redundss3  39211  l1cvat  39679  pmod2iN  40473  pmodN  40474  pmodl42N  40475  osumcllem3N  40582  osumcllem4N  40583  dihmeetlem19N  41949  dihmeetALTN  41951  readvrec2  42970  elrfi  43275  diophrw  43340  eldioph2lem1  43341  eldioph2lem2  43342  diophin  43353  diophren  43390  dnwech  43625  fnwe2lem2  43628  kelac2lem  43641  kelac2  43642  lmhmlnmsplit  43664  pwssplit4  43666  pwfi2f1o  43673  proot1hash  43772  naddov4  43960  rp-fakeuninass  44092  elcnvcnvintab  44158  relintab  44159  elcnvcnvlem  44175  conrel1d  44239  dfrcl2  44250  iunrelexp0  44278  ntrk0kbimka  44615  hashnzfz  44896  zfregs2VD  45416  iunconnlem2  45510  ssinss2d  45640  restuni4  45699  restuni6  45700  restsubel  45731  iccdifioo  46091  uzinico2  46137  sumnnodd  46206  cncfuni  46460  fouriersw  46805  saliinclf  46900  iundjiunlem  47033  iundjiun  47034  caragenuncllem  47086  caragendifcl  47088  hoidmvlelem2  47170  smflimlem1  47345  3f1oss1  47669  perfectALTVlem2  48344  rngchomrnghmresALTV  48901  rngcrescrhmALTV  48902  rhmsubcALTVlem3  48905  rhmsubcALTVlem4  48906  resinsn  49493  resinsnALT  49494  tposrescnv  49500  opndisj  49524  restclssep  49537  seposep  49547  iscnrm3rlem3  49563  iscnrm3rlem8  49568  oppczeroo  49858