Theorem incom 4159

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  {crab 3397   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-rab 3398  df-in 3906

This theorem is referenced by:  ineqcom  4160  ineqcomi  4161  ineq2  4164  sseqin2  4173  in12  4179  in32  4180  in13  4181  in31  4182  inss2  4188  sslin  4193  inss  4198  dfss7  4201  indif1  4232  indifcom  4233  indir  4236  indifdir  4245  dfsymdif3  4256  dfrab2  4270  0in  4347  disjr  4401  disjdifr  4423  difdifdir  4442  uneqdifeq  4443  disjtp2  4671  iinrab2  5023  iunin1  5025  iinin1  5032  riinn0  5036  disjprg  5092  disjxun  5094  inex2  5261  inex2g  5263  rescom  5959  resindm  5987  resdmdfsn  5988  resopab  5991  imadisj  6037  intirr  6073  djudisj  6123  imainrect  6137  dmresv  6156  resdmres  6188  coeq0  6212  dfpred3  6268  predres  6295  frpoind  6298  ordtri3or  6347  fnresdisj  6610  fnimaeq0  6623  resasplit  6702  fresaun  6703  fresaunres2  6704  fresaunres1  6705  f0rn0  6717  fvun2  6924  rescnvimafod  7016  fveqressseq  7022  ressnop0  7096  fninfp  7118  fsnunfv  7131  orduniss2  7773  offres  7925  curry1  8044  curry2  8047  fpar  8056  fprlem1  8240  smores3  8283  oacomf1o  8490  domunsncan  9003  dif1ennnALT  9175  domunfican  9220  marypha1lem  9334  zfregfr  9511  epfrs  9638  zfregs2  9640  frind  9660  frrlem15  9667  djuin  9828  tskwe  9860  dfac8b  9939  ac10ct  9942  kmlem11  10069  kmlem12  10070  djucomen  10086  onadju  10102  ackbij1lem14  10140  ackbij1lem16  10142  fin23lem26  10233  fin23lem19  10244  fin23lem30  10250  isf32lem4  10264  isf34lem7  10287  isf34lem6  10288  axdc3lem4  10361  brdom7disj  10439  brdom6disj  10440  fpwwe2lem12  10551  fzpreddisj  13487  fzdifsuc  13498  fseq1p1m1  13512  prinfzo0  13612  hashun3  14305  hashbclem  14373  hash7g  14407  xpcoidgend  14896  cotr2  14898  limsupgle  15398  prmreclem2  16843  setsdm  17095  ressinbas  17170  wunress  17174  mreexexlem2d  17566  oppcinv  17702  cnvps  18499  pmtrmvd  19383  lsmmod2  19603  lsmdisj3  19610  lsmdisjr  19611  lsmdisj2r  19612  lsmdisj3r  19613  lsmdisj2a  19614  lsmdisj2b  19615  lsmdisj3a  19616  lsmdisj3b  19617  subgdisj2  19619  pj2f  19625  pj1id  19626  frgpuplem  19699  gsummptfzsplitl  19860  dprd2da  19971  dmdprdsplit2lem  19974  dmdprdsplit2  19975  pgpfaclem1  20010  rnghmsscmap2  20560  rnghmsubcsetclem1  20562  rnghmsubcsetc  20564  rngccat  20565  rngcid  20566  rngcifuestrc  20570  funcrngcsetc  20571  rhmsscmap2  20589  rhmsubcsetclem1  20591  rhmsubcsetc  20593  ringccat  20594  ringcid  20595  rhmsscrnghm  20596  rhmsubcrngclem1  20597  rhmsubcrngc  20599  rngcresringcat  20600  funcringcsetc  20605  rngcrescrhm  20615  rhmsubclem3  20618  rhmsubc  20620  lmhmlsp  20999  psgndiflemB  21553  pjpm  21661  ltbwe  21997  psrbag0  22015  elcls  23015  mretopd  23034  restin  23108  restcld  23114  resstopn  23128  lecldbas  23161  nrmsep  23299  isreg2  23319  ordthaus  23326  cmpsublem  23341  cmpsub  23342  hauscmplem  23348  bwth  23352  iunconn  23370  cldllycmp  23437  kgentopon  23480  llycmpkgen2  23492  1stckgen  23496  txkgen  23594  kqcldsat  23675  regr1lem2  23682  fbun  23782  fin1aufil  23874  fclsfnflim  23969  ustexsym  24158  restutopopn  24180  ustuqtop5  24187  ressuss  24204  metreslem  24304  blcld  24447  ressxms  24467  ressms  24468  reconn  24771  metdseq0  24797  metnrmlem3  24804  unmbl  25492  volun  25500  iundisj2  25504  icombl  25519  ioombl  25520  uniioombllem2  25538  uniioombllem4  25541  dyaddisjlem  25550  dyaddisj  25551  mbfconstlem  25582  mbfeqalem2  25597  ismbf3d  25609  itg1addlem5  25655  itgsplitioo  25793  lhop  25975  vieta1lem2  26273  perfectlem2  27195  rplogsum  27492  nosupbnd2lem1  27681  sltlpss  27880  slelss  27881  perpcom  28734  vtxdgoddnumeven  29576  ex-dif  30447  ococi  31429  orthin  31470  lediri  31561  pjoml2i  31609  pjoml4i  31611  cmcmlem  31615  cmbr3i  31624  cmm2i  31631  cm0  31633  fh1  31642  fh2  31643  cm2j  31644  qlaxr3i  31660  pjclem2  32220  stm1ri  32268  golem1  32295  dmdbr5  32332  mddmd2  32333  cvmdi  32348  mdsldmd1i  32355  csmdsymi  32358  mdexchi  32359  cvexchi  32393  atssma  32402  atomli  32406  atoml2i  32407  atordi  32408  atcvatlem  32409  chirredlem1  32414  chirredlem2  32415  chirredlem3  32416  atcvat4i  32421  atabsi  32425  mdsymlem1  32427  dmdbr6ati  32447  cdj3lem3  32462  inin  32540  difuncomp  32577  iundisj2f  32614  disjunsn  32618  imadifxp  32625  fnresin  32651  mptiffisupp  32721  mptprop  32726  df1stres  32732  df2ndres  32733  padct  32746  iocinif  32810  difioo  32811  fzodif1  32821  iundisj2fi  32826  xrge00  33045  symgcom  33114  cycpm2tr  33150  cycpmco2f1  33155  xrge0slmod  33378  ssdifidlprm  33488  oppr2idl  33516  ufdprmidl  33571  1arithufdlem4  33577  psrbasfsupp  33642  lindsun  33731  fldexttr  33764  lmxrge0  34058  esumrnmpt2  34174  esumpfinvallem  34180  ldgenpisyslem1  34269  ldgenpisys  34272  measxun2  34316  measunl  34322  carsgclctunlem1  34423  carsgclctunlem2  34425  eulerpartlemt  34477  eulerpartgbij  34478  probmeasb  34536  bayesth  34545  ballotlemfp1  34598  ballotlemfval0  34602  signstres  34681  hashreprin  34726  reprfz1  34730  chtvalz  34735  breprexpnat  34740  f1resrcmplf1d  35192  f1resfz0f1d  35257  subfacp1lem3  35325  subfacp1lem5  35327  pconnconn  35374  cvmscld  35416  cvmsss2  35417  satef  35559  satefvfmla0  35561  mrsubvrs  35665  cldbnd  36469  bj-inrab3  37073  bj-2upln1upl  37168  bj-sscon  37173  bj-rest0  37237  bj-0int  37245  bj-ismooredr2  37254  icoreclin  37501  fin2so  37747  ptrest  37759  poimirlem3  37763  poimirlem11  37771  poimirlem12  37772  poimirlem13  37773  poimirlem14  37774  poimirlem15  37775  poimirlem18  37778  poimirlem21  37781  poimirlem22  37782  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  cnambfre  37808  asindmre  37843  dvasin  37844  dvreasin  37846  dvreacos  37847  sstotbnd2  37914  bndss  37926  inres2  38382  disjressuc2  38535  redundss3  38824  l1cvat  39254  pmod2iN  40048  pmodN  40049  pmodl42N  40050  osumcllem3N  40157  osumcllem4N  40158  dihmeetlem19N  41524  dihmeetALTN  41526  readvrec2  42558  elrfi  42878  diophrw  42943  eldioph2lem1  42944  eldioph2lem2  42945  diophin  42956  diophren  42997  dnwech  43232  fnwe2lem2  43235  kelac2lem  43248  kelac2  43249  lmhmlnmsplit  43271  pwssplit4  43273  pwfi2f1o  43280  proot1hash  43379  naddov4  43567  rp-fakeuninass  43699  elcnvcnvintab  43765  relintab  43766  elcnvcnvlem  43782  conrel1d  43846  dfrcl2  43857  iunrelexp0  43885  ntrk0kbimka  44222  hashnzfz  44503  zfregs2VD  45023  iunconnlem2  45117  ssinss2d  45247  restuni4  45307  restuni6  45308  restsubel  45339  iccdifioo  45703  uzinico2  45749  sumnnodd  45818  limsupvaluz  45894  cncfuni  46072  fouriersw  46417  saliinclf  46512  iundjiunlem  46645  iundjiun  46646  caragenuncllem  46698  caragendifcl  46700  hoidmvlelem2  46782  smflimlem1  46957  3f1oss1  47263  perfectALTVlem2  47910  rngchomrnghmresALTV  48467  rngcrescrhmALTV  48468  rhmsubcALTVlem3  48471  rhmsubcALTVlem4  48472  resinsn  49059  resinsnALT  49060  tposrescnv  49066  opndisj  49090  restclssep  49103  seposep  49113  iscnrm3rlem3  49129  iscnrm3rlem8  49134  oppczeroo  49424