Theorem incom 4182

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  {crab 3413   ∩ cin 3923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-rab 3414  df-in 3931

This theorem is referenced by:  ineqcom  4183  ineqcomi  4184  ineq2  4187  sseqin2  4196  in12  4202  in32  4203  in13  4204  in31  4205  inss2  4211  sslin  4216  inss  4221  dfss7  4224  indif1  4255  indifcom  4256  indir  4259  indifdir  4268  dfsymdif3  4279  dfrab2  4293  0in  4370  disjr  4424  disjdifr  4446  difdifdir  4465  uneqdifeq  4466  disjtp2  4689  iinrab2  5043  iunin1  5045  iinin1  5052  riinn0  5056  disjprg  5112  disjxun  5114  inex2  5285  inex2g  5287  rescom  5986  resindm  6014  resdmdfsn  6015  resopab  6018  imadisj  6064  intirr  6104  djudisj  6153  imainrect  6167  dmresv  6186  resdmres  6218  coeq0  6241  dfpred3  6298  predres  6325  frpoind  6328  wfiOLD  6337  ordtri3or  6381  fnresdisj  6654  fnimaeq0  6667  resasplit  6744  fresaun  6745  fresaunres2  6746  fresaunres1  6747  f0rn0  6759  fvun2  6967  rescnvimafod  7059  fveqressseq  7065  ressnop0  7139  fninfp  7162  fsnunfv  7175  orduniss2  7821  offres  7976  curry1  8097  curry2  8100  fpar  8109  fprlem1  8293  wfrlem5OLD  8321  smores3  8361  oacomf1o  8571  domunsncan  9080  phplem2OLD  9223  dif1ennnALT  9277  domunfican  9327  marypha1lem  9439  zfregfr  9611  epfrs  9737  zfregs2  9739  frind  9756  frrlem15  9763  djuin  9924  tskwe  9956  dfac8b  10037  ac10ct  10040  kmlem11  10167  kmlem12  10168  djucomen  10184  onadju  10200  ackbij1lem14  10238  ackbij1lem16  10240  fin23lem26  10331  fin23lem19  10342  fin23lem30  10348  isf32lem4  10362  isf34lem7  10385  isf34lem6  10386  axdc3lem4  10459  brdom7disj  10537  brdom6disj  10538  fpwwe2lem12  10648  fzpreddisj  13579  fzdifsuc  13590  fseq1p1m1  13604  prinfzo0  13704  hashun3  14390  hashbclem  14458  hash7g  14492  xpcoidgend  14981  cotr2  14983  limsupgle  15480  prmreclem2  16922  setsdm  17174  ressinbas  17251  wunress  17255  mreexexlem2d  17642  oppcinv  17778  cnvps  18573  pmtrmvd  19422  lsmmod2  19642  lsmdisj3  19649  lsmdisjr  19650  lsmdisj2r  19651  lsmdisj3r  19652  lsmdisj2a  19653  lsmdisj2b  19654  lsmdisj3a  19655  lsmdisj3b  19656  subgdisj2  19658  pj2f  19664  pj1id  19665  frgpuplem  19738  gsummptfzsplitl  19899  dprd2da  20010  dmdprdsplit2lem  20013  dmdprdsplit2  20014  pgpfaclem1  20049  rnghmsscmap2  20574  rnghmsubcsetclem1  20576  rnghmsubcsetc  20578  rngccat  20579  rngcid  20580  rngcifuestrc  20584  funcrngcsetc  20585  rhmsscmap2  20603  rhmsubcsetclem1  20605  rhmsubcsetc  20607  ringccat  20608  ringcid  20609  rhmsscrnghm  20610  rhmsubcrngclem1  20611  rhmsubcrngc  20613  rngcresringcat  20614  funcringcsetc  20619  rngcrescrhm  20629  rhmsubclem3  20632  rhmsubc  20634  lmhmlsp  20992  psgndiflemB  21545  pjpm  21653  ltbwe  21987  psrbag0  22005  elcls  22996  mretopd  23015  restin  23089  restcld  23095  resstopn  23109  lecldbas  23142  nrmsep  23280  isreg2  23300  ordthaus  23307  cmpsublem  23322  cmpsub  23323  hauscmplem  23329  bwth  23333  iunconn  23351  cldllycmp  23418  kgentopon  23461  llycmpkgen2  23473  1stckgen  23477  txkgen  23575  kqcldsat  23656  regr1lem2  23663  fbun  23763  fin1aufil  23855  fclsfnflim  23950  ustexsym  24139  restutopopn  24162  ustuqtop5  24169  ressuss  24186  metreslem  24286  blcld  24429  ressxms  24449  ressms  24450  reconn  24753  metdseq0  24779  metnrmlem3  24786  unmbl  25475  volun  25483  iundisj2  25487  icombl  25502  ioombl  25503  uniioombllem2  25521  uniioombllem4  25524  dyaddisjlem  25533  dyaddisj  25534  mbfconstlem  25565  mbfeqalem2  25580  ismbf3d  25592  itg1addlem5  25638  itgsplitioo  25776  lhop  25958  vieta1lem2  26256  xrlimcnp  26914  perfectlem2  27177  rplogsum  27474  nosupbnd2lem1  27663  sltlpss  27848  slelss  27849  perpcom  28624  vtxdgoddnumeven  29465  ex-dif  30336  ococi  31318  orthin  31359  lediri  31450  pjoml2i  31498  pjoml4i  31500  cmcmlem  31504  cmbr3i  31513  cmm2i  31520  cm0  31522  fh1  31531  fh2  31532  cm2j  31533  qlaxr3i  31549  pjclem2  32109  stm1ri  32157  golem1  32184  dmdbr5  32221  mddmd2  32222  cvmdi  32237  mdsldmd1i  32244  csmdsymi  32247  mdexchi  32248  cvexchi  32282  atssma  32291  atomli  32295  atoml2i  32296  atordi  32297  atcvatlem  32298  chirredlem1  32303  chirredlem2  32304  chirredlem3  32305  atcvat4i  32310  atabsi  32314  mdsymlem1  32316  dmdbr6ati  32336  cdj3lem3  32351  inin  32429  difuncomp  32467  iundisj2f  32504  disjunsn  32508  imadifxp  32515  fnresin  32537  mptiffisupp  32603  mptprop  32608  df1stres  32614  df2ndres  32615  padct  32632  iocinif  32692  difioo  32693  fzodif1  32703  iundisj2fi  32708  xrge00  32926  symgcom  33012  cycpm2tr  33048  cycpmco2f1  33053  xrge0slmod  33281  ssdifidlprm  33391  oppr2idl  33419  ufdprmidl  33474  1arithufdlem4  33480  lindsun  33581  fldexttr  33616  lmxrge0  33891  esumrnmpt2  34007  esumpfinvallem  34013  ldgenpisyslem1  34102  ldgenpisys  34105  measxun2  34149  measunl  34155  carsgclctunlem1  34257  carsgclctunlem2  34259  eulerpartlemt  34311  eulerpartgbij  34312  probmeasb  34370  bayesth  34379  ballotlemfp1  34432  ballotlemfval0  34436  signstres  34528  hashreprin  34573  reprfz1  34577  chtvalz  34582  breprexpnat  34587  f1resrcmplf1d  35039  f1resfz0f1d  35057  subfacp1lem3  35125  subfacp1lem5  35127  pconnconn  35174  cvmscld  35216  cvmsss2  35217  satef  35359  satefvfmla0  35361  mrsubvrs  35465  cldbnd  36265  bj-inrab3  36868  bj-2upln1upl  36963  bj-sscon  36968  bj-rest0  37032  bj-0int  37040  bj-ismooredr2  37049  icoreclin  37296  fin2so  37552  ptrest  37564  poimirlem3  37568  poimirlem11  37576  poimirlem12  37577  poimirlem13  37578  poimirlem14  37579  poimirlem15  37580  poimirlem18  37583  poimirlem21  37586  poimirlem22  37587  mblfinlem3  37604  mblfinlem4  37605  ismblfin  37606  cnambfre  37613  asindmre  37648  dvasin  37649  dvreasin  37651  dvreacos  37652  sstotbnd2  37719  bndss  37731  inres2  38185  disjressuc2  38327  redundss3  38567  l1cvat  38994  pmod2iN  39789  pmodN  39790  pmodl42N  39791  osumcllem3N  39898  osumcllem4N  39899  dihmeetlem19N  41265  dihmeetALTN  41267  metakunt18  42157  readvrec2  42329  elrfi  42642  diophrw  42707  eldioph2lem1  42708  eldioph2lem2  42709  diophin  42720  diophren  42761  dnwech  42997  fnwe2lem2  43000  kelac2lem  43013  kelac2  43014  lmhmlnmsplit  43036  pwssplit4  43038  pwfi2f1o  43045  proot1hash  43144  naddov4  43332  rp-fakeuninass  43465  elcnvcnvintab  43531  relintab  43532  elcnvcnvlem  43548  conrel1d  43612  dfrcl2  43623  iunrelexp0  43651  ntrk0kbimka  43988  hashnzfz  44270  zfregs2VD  44792  iunconnlem2  44886  ssinss2d  45011  restuni4  45072  restuni6  45073  restsubel  45104  iccdifioo  45472  uzinico2  45519  sumnnodd  45589  limsupvaluz  45667  cncfuni  45845  fouriersw  46190  saliinclf  46285  iundjiunlem  46418  iundjiun  46419  caragenuncllem  46471  caragendifcl  46473  hoidmvlelem2  46555  smflimlem1  46730  3f1oss1  47032  perfectALTVlem2  47654  rngchomrnghmresALTV  48140  rngcrescrhmALTV  48141  rhmsubcALTVlem3  48144  rhmsubcALTVlem4  48145  resinsn  48727  resinsnALT  48728  tposrescnv  48734  opndisj  48756  restclssep  48769  seposep  48779  iscnrm3rlem3  48795  iscnrm3rlem8  48800  oppczeroo  48960