Theorem incom 4216

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  {crab 3432   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-rab 3433  df-in 3969

This theorem is referenced by:  ineqcom  4217  ineqcomi  4218  ineq2  4221  sseqin2  4230  in12  4236  in32  4237  in13  4238  in31  4239  inss2  4245  sslin  4250  inss  4254  dfss7  4256  indif1  4287  indifcom  4288  indir  4291  indifdir  4300  dfsymdif3  4311  dfrab2  4325  0in  4402  disjr  4456  disjdifr  4478  difdifdir  4497  uneqdifeq  4498  disjtp2  4720  iinrab2  5074  iunin1  5076  iinin1  5083  riinn0  5087  disjprg  5143  disjxun  5145  inex2  5323  inex2g  5325  rescom  6022  resindm  6049  resdmdfsn  6050  resopab  6053  imadisj  6099  intirr  6140  djudisj  6188  imainrect  6202  dmresv  6221  resdmres  6253  coeq0  6276  dfpred3  6333  predres  6361  frpoind  6364  wfiOLD  6373  ordtri3or  6417  fnresdisj  6688  fnimaeq0  6701  resasplit  6778  fresaun  6779  fresaunres2  6780  fresaunres1  6781  f0rn0  6793  fvun2  7000  rescnvimafod  7092  fveqressseq  7098  ressnop0  7172  fninfp  7193  fsnunfv  7206  orduniss2  7852  offres  8006  curry1  8127  curry2  8130  fpar  8139  fprlem1  8323  wfrlem5OLD  8351  smores3  8391  oacomf1o  8601  domunsncan  9110  phplem2OLD  9252  dif1ennnALT  9308  domunfican  9358  marypha1lem  9470  zfregfr  9642  epfrs  9768  zfregs2  9770  frind  9787  frrlem15  9794  djuin  9955  tskwe  9987  dfac8b  10068  ac10ct  10071  kmlem11  10198  kmlem12  10199  djucomen  10215  onadju  10231  ackbij1lem14  10269  ackbij1lem16  10271  fin23lem26  10362  fin23lem19  10373  fin23lem30  10379  isf32lem4  10393  isf34lem7  10416  isf34lem6  10417  axdc3lem4  10490  brdom7disj  10568  brdom6disj  10569  fpwwe2lem12  10679  fzpreddisj  13609  fzdifsuc  13620  fseq1p1m1  13634  prinfzo0  13734  hashun3  14419  hashbclem  14487  hash7g  14521  xpcoidgend  15010  cotr2  15012  limsupgle  15509  prmreclem2  16950  setsdm  17203  ressinbas  17290  wunress  17295  wunressOLD  17296  mreexexlem2d  17689  oppcinv  17827  cnvps  18635  pmtrmvd  19488  lsmmod2  19708  lsmdisj3  19715  lsmdisjr  19716  lsmdisj2r  19717  lsmdisj3r  19718  lsmdisj2a  19719  lsmdisj2b  19720  lsmdisj3a  19721  lsmdisj3b  19722  subgdisj2  19724  pj2f  19730  pj1id  19731  frgpuplem  19804  gsummptfzsplitl  19965  dprd2da  20076  dmdprdsplit2lem  20079  dmdprdsplit2  20080  pgpfaclem1  20115  rnghmsscmap2  20645  rnghmsubcsetclem1  20647  rnghmsubcsetc  20649  rngccat  20650  rngcid  20651  rngcifuestrc  20655  funcrngcsetc  20656  rhmsscmap2  20674  rhmsubcsetclem1  20676  rhmsubcsetc  20678  ringccat  20679  ringcid  20680  rhmsscrnghm  20681  rhmsubcrngclem1  20682  rhmsubcrngc  20684  rngcresringcat  20685  funcringcsetc  20690  rngcrescrhm  20700  rhmsubclem3  20703  rhmsubc  20705  lmhmlsp  21065  cnfldfunALTOLDOLD  21410  psgndiflemB  21635  pjpm  21745  ltbwe  22079  psrbag0  22103  elcls  23096  mretopd  23115  restin  23189  restcld  23195  resstopn  23209  lecldbas  23242  nrmsep  23380  isreg2  23400  ordthaus  23407  cmpsublem  23422  cmpsub  23423  hauscmplem  23429  bwth  23433  iunconn  23451  cldllycmp  23518  kgentopon  23561  llycmpkgen2  23573  1stckgen  23577  txkgen  23675  kqcldsat  23756  regr1lem2  23763  fbun  23863  fin1aufil  23955  fclsfnflim  24050  ustexsym  24239  restutopopn  24262  ustuqtop5  24269  ressuss  24286  metreslem  24387  blcld  24533  ressxms  24553  ressms  24554  reconn  24863  metdseq0  24889  metnrmlem3  24896  unmbl  25585  volun  25593  iundisj2  25597  icombl  25612  ioombl  25613  uniioombllem2  25631  uniioombllem4  25634  dyaddisjlem  25643  dyaddisj  25644  mbfconstlem  25675  mbfeqalem2  25690  ismbf3d  25702  itg1addlem5  25749  itgsplitioo  25887  lhop  26069  vieta1lem2  26367  xrlimcnp  27025  perfectlem2  27288  rplogsum  27585  nosupbnd2lem1  27774  sltlpss  27959  slelss  27960  perpcom  28735  vtxdgoddnumeven  29585  ex-dif  30451  ococi  31433  orthin  31474  lediri  31565  pjoml2i  31613  pjoml4i  31615  cmcmlem  31619  cmbr3i  31628  cmm2i  31635  cm0  31637  fh1  31646  fh2  31647  cm2j  31648  qlaxr3i  31664  pjclem2  32224  stm1ri  32272  golem1  32299  dmdbr5  32336  mddmd2  32337  cvmdi  32352  mdsldmd1i  32359  csmdsymi  32362  mdexchi  32363  cvexchi  32397  atssma  32406  atomli  32410  atoml2i  32411  atordi  32412  atcvatlem  32413  chirredlem1  32418  chirredlem2  32419  chirredlem3  32420  atcvat4i  32425  atabsi  32429  mdsymlem1  32431  dmdbr6ati  32451  cdj3lem3  32466  inin  32543  difuncomp  32573  iundisj2f  32609  disjunsn  32613  imadifxp  32620  fnresin  32642  mptiffisupp  32707  mptprop  32712  df1stres  32718  df2ndres  32719  padct  32736  iocinif  32789  difioo  32790  fzodif1  32800  iundisj2fi  32804  xrge00  32999  symgcom  33085  cycpm2tr  33121  cycpmco2f1  33126  xrge0slmod  33355  ssdifidlprm  33465  oppr2idl  33493  ufdprmidl  33548  1arithufdlem4  33554  lindsun  33652  fldexttr  33685  lmxrge0  33912  esumrnmpt2  34048  esumpfinvallem  34054  ldgenpisyslem1  34143  ldgenpisys  34146  measxun2  34190  measunl  34196  carsgclctunlem1  34298  carsgclctunlem2  34300  eulerpartlemt  34352  eulerpartgbij  34353  probmeasb  34411  bayesth  34420  ballotlemfp1  34472  ballotlemfval0  34476  signstres  34568  hashreprin  34613  reprfz1  34617  chtvalz  34622  breprexpnat  34627  f1resrcmplf1d  35079  f1resfz0f1d  35097  subfacp1lem3  35166  subfacp1lem5  35168  pconnconn  35215  cvmscld  35257  cvmsss2  35258  satef  35400  satefvfmla0  35402  mrsubvrs  35506  cldbnd  36308  bj-inrab3  36911  bj-2upln1upl  37006  bj-sscon  37011  bj-rest0  37075  bj-0int  37083  bj-ismooredr2  37092  icoreclin  37339  fin2so  37593  ptrest  37605  poimirlem3  37609  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  cnambfre  37654  asindmre  37689  dvasin  37690  dvreasin  37692  dvreacos  37693  sstotbnd2  37760  bndss  37772  inres2  38226  disjressuc2  38369  redundss3  38609  l1cvat  39036  pmod2iN  39831  pmodN  39832  pmodl42N  39833  osumcllem3N  39940  osumcllem4N  39941  dihmeetlem19N  41307  dihmeetALTN  41309  metakunt18  42203  readvrec2  42369  elrfi  42681  diophrw  42746  eldioph2lem1  42747  eldioph2lem2  42748  diophin  42759  diophren  42800  dnwech  43036  fnwe2lem2  43039  kelac2lem  43052  kelac2  43053  lmhmlnmsplit  43075  pwssplit4  43077  pwfi2f1o  43084  proot1hash  43183  naddov4  43372  rp-fakeuninass  43505  elcnvcnvintab  43571  relintab  43572  elcnvcnvlem  43588  conrel1d  43652  dfrcl2  43663  iunrelexp0  43691  ntrk0kbimka  44028  hashnzfz  44315  zfregs2VD  44838  iunconnlem2  44932  ssinss2d  44999  restuni4  45060  restuni6  45061  restsubel  45095  iccdifioo  45467  uzinico2  45514  sumnnodd  45585  limsupvaluz  45663  cncfuni  45841  fouriersw  46186  saliinclf  46281  iundjiunlem  46414  iundjiun  46415  caragenuncllem  46467  caragendifcl  46469  hoidmvlelem2  46551  smflimlem1  46726  3f1oss1  47024  perfectALTVlem2  47646  rngchomrnghmresALTV  48122  rngcrescrhmALTV  48123  rhmsubcALTVlem3  48126  rhmsubcALTVlem4  48127  opndisj  48698  restclssep  48711  seposep  48721  iscnrm3rlem3  48738  iscnrm3rlem8  48743