Theorem incom 4138

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

Syntax hints:   = wceq 1547   ∈ wcel 2119  {crab 3391   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-rab 3392  df-in 3890

This theorem is referenced by:  ineqcom  4139  ineqcomi  4140  ineq2  4143  in12  4157  in32  4158  in13  4159  in31  4160  inss2  4166  sslin  4171  inss  4176  indif1  4210  indifcom  4211  indir  4214  indifdir  4223  dfsymdif3  4234  dfrab2  4248  difdifdir  4419  disjtp2  4648  iunin1  5001  iinin1  5008  riinn0  5012  disjprg  5068  disjxun  5070  inex2  5246  inex2g  5248  rescom  5954  resindm  5982  resdmdfsn  5983  resopab  5986  imadisj  6032  intirr  6068  djudisj  6118  imainrect  6132  dmresv  6151  resdmres  6183  coeq0  6207  dfpred3  6263  predres  6290  frpoind  6293  ordtri3or  6342  fnresdisj  6605  fnimaeq0  6618  resasplit  6697  fresaun  6698  fresaunres2  6699  fresaunres1  6700  f0rn0  6712  fvun2  6919  rescnvimafod  7014  fveqressseq  7020  ressnop0  7096  fninfp  7118  fsnunfv  7131  orduniss2  7773  offres  7925  curry1  8043  curry2  8046  fpar  8055  fprlem1  8240  smores3  8283  oacomf1o  8490  domunsncan  9005  dif1ennnALT  9177  domunfican  9222  marypha1lem  9336  zfregfr  9516  epfrs  9643  zfregs2  9645  frind  9665  frrlem15  9672  djuin  9833  tskwe  9865  dfac8b  9944  ac10ct  9947  kmlem11  10074  kmlem12  10075  djucomen  10091  onadju  10107  ackbij1lem14  10145  ackbij1lem16  10147  fin23lem26  10238  fin23lem19  10249  fin23lem30  10255  isf32lem4  10269  isf34lem7  10292  isf34lem6  10293  axdc3lem4  10366  brdom7disj  10444  brdom6disj  10445  fpwwe2lem12  10556  fzpreddisj  13518  fzdifsuc  13529  fseq1p1m1  13543  prinfzo0  13644  hashun3  14337  hashbclem  14405  hash7g  14439  xpcoidgend  14928  cotr2  14930  limsupgle  15430  prmreclem2  16879  setsdm  17131  ressinbas  17206  wunress  17210  mreexexlem2d  17602  oppcinv  17738  cnvps  18535  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  20601  rnghmsubcsetclem1  20603  rnghmsubcsetc  20605  rngccat  20606  rngcid  20607  rngcifuestrc  20611  funcrngcsetc  20612  rhmsscmap2  20630  rhmsubcsetclem1  20632  rhmsubcsetc  20634  ringccat  20635  ringcid  20636  rhmsscrnghm  20637  rhmsubcrngclem1  20638  rhmsubcrngc  20640  rngcresringcat  20641  funcringcsetc  20646  rngcrescrhm  20656  rhmsubclem3  20659  rhmsubc  20661  lmhmlsp  21039  psgndiflemB  21575  pjpm  21683  ltbwe  22020  psrbag0  22038  elcls  23056  mretopd  23075  restin  23149  restcld  23155  resstopn  23169  lecldbas  23202  nrmsep  23340  isreg2  23360  ordthaus  23367  cmpsublem  23382  cmpsub  23383  hauscmplem  23389  bwth  23393  iunconn  23411  cldllycmp  23478  kgentopon  23521  llycmpkgen2  23533  1stckgen  23537  txkgen  23635  kqcldsat  23716  regr1lem2  23723  fbun  23823  fin1aufil  23915  fclsfnflim  24010  ustexsym  24199  restutopopn  24221  ustuqtop5  24228  ressuss  24245  metreslem  24345  blcld  24488  ressxms  24508  ressms  24509  reconn  24812  metdseq0  24838  metnrmlem3  24845  unmbl  25522  volun  25530  iundisj2  25534  icombl  25549  ioombl  25550  uniioombllem2  25568  uniioombllem4  25571  dyaddisjlem  25580  dyaddisj  25581  mbfconstlem  25612  mbfeqalem2  25627  ismbf3d  25639  itg1addlem5  25685  itgsplitioo  25823  lhop  26001  vieta1lem2  26295  perfectlem2  27211  rplogsum  27508  nosupbnd2lem1  27697  ltslpss  27918  leslss  27919  perpcom  28799  vtxdgoddnumeven  29640  ex-dif  30511  ococi  31494  orthin  31535  lediri  31626  pjoml2i  31674  pjoml4i  31676  cmcmlem  31680  cmbr3i  31689  cmm2i  31696  cm0  31698  fh1  31707  fh2  31708  cm2j  31709  qlaxr3i  31725  pjclem2  32285  stm1ri  32333  golem1  32360  dmdbr5  32397  mddmd2  32398  cvmdi  32413  mdsldmd1i  32420  csmdsymi  32423  mdexchi  32424  cvexchi  32458  atssma  32467  atomli  32471  atoml2i  32472  atordi  32473  atcvatlem  32474  chirredlem1  32479  chirredlem2  32480  chirredlem3  32481  atcvat4i  32486  atabsi  32490  mdsymlem1  32492  dmdbr6ati  32512  cdj3lem3  32527  inin  32604  difuncomp  32642  iundisj2f  32679  disjunsn  32683  imadifxp  32690  fnresin  32716  mptiffisupp  32785  mptprop  32790  df1stres  32796  df2ndres  32797  iocinif  32873  difioo  32874  fzodif1  32884  iundisj2fi  32889  xrge00  33093  symgcom  33164  cycpm2tr  33200  cycpmco2f1  33205  xrge0slmod  33431  ssdifidlprm  33541  oppr2idl  33569  ufdprmidl  33624  1arithufdlem4  33630  psrbasfsupp  33695  lindsun  33809  fldexttr  33842  lmxrge0  34136  esumrnmpt2  34252  esumpfinvallem  34258  ldgenpisyslem1  34347  ldgenpisys  34350  measxun2  34394  measunl  34400  carsgclctunlem1  34501  carsgclctunlem2  34503  eulerpartlemt  34555  eulerpartgbij  34556  probmeasb  34614  bayesth  34623  ballotlemfp1  34676  ballotlemfval0  34680  signstres  34759  hashreprin  34804  reprfz1  34808  chtvalz  34813  breprexpnat  34818  f1resrcmplf1d  35268  f1resfz0f1d  35342  subfacp1lem3  35410  subfacp1lem5  35412  pconnconn  35459  cvmscld  35501  cvmsss2  35502  satef  35644  satefvfmla0  35646  mrsubvrs  35750  cldbnd  36554  bj-inrab3  37282  bj-2upln1upl  37377  bj-sscon  37382  bj-rest0  37451  bj-0int  37459  bj-ismooredr2  37468  icoreclin  37719  fin2so  37974  ptrest  37986  poimirlem3  37990  poimirlem11  37998  poimirlem12  37999  poimirlem13  38000  poimirlem14  38001  poimirlem15  38002  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  cnambfre  38035  asindmre  38070  dvasin  38071  dvreasin  38073  dvreacos  38074  sstotbnd2  38141  bndss  38153  inres2  38614  disjressuc2  38778  redundss3  39079  l1cvat  39547  pmod2iN  40341  pmodN  40342  pmodl42N  40343  osumcllem3N  40450  osumcllem4N  40451  dihmeetlem19N  41817  dihmeetALTN  41819  readvrec2  42838  elrfi  43143  diophrw  43208  eldioph2lem1  43209  eldioph2lem2  43210  diophin  43221  diophren  43258  dnwech  43493  fnwe2lem2  43496  kelac2lem  43509  kelac2  43510  lmhmlnmsplit  43532  pwssplit4  43534  pwfi2f1o  43541  proot1hash  43640  naddov4  43828  rp-fakeuninass  43960  elcnvcnvintab  44026  relintab  44027  elcnvcnvlem  44043  conrel1d  44107  dfrcl2  44118  iunrelexp0  44146  ntrk0kbimka  44483  hashnzfz  44764  zfregs2VD  45284  iunconnlem2  45378  ssinss2d  45508  restuni4  45568  restuni6  45569  restsubel  45600  iccdifioo  45960  uzinico2  46006  sumnnodd  46075  limsupvaluz  46151  cncfuni  46329  fouriersw  46674  saliinclf  46769  iundjiunlem  46902  iundjiun  46903  caragenuncllem  46955  caragendifcl  46957  hoidmvlelem2  47039  smflimlem1  47214  3f1oss1  47538  perfectALTVlem2  48213  rngchomrnghmresALTV  48770  rngcrescrhmALTV  48771  rhmsubcALTVlem3  48774  rhmsubcALTVlem4  48775  resinsn  49362  resinsnALT  49363  tposrescnv  49369  opndisj  49393  restclssep  49406  seposep  49416  iscnrm3rlem3  49432  iscnrm3rlem8  49437  oppczeroo  49727