Theorem incom 4189

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  {crab 3420   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-rab 3421  df-in 3938

This theorem is referenced by:  ineqcom  4190  ineqcomi  4191  ineq2  4194  sseqin2  4203  in12  4209  in32  4210  in13  4211  in31  4212  inss2  4218  sslin  4223  inss  4228  dfss7  4231  indif1  4262  indifcom  4263  indir  4266  indifdir  4275  dfsymdif3  4286  dfrab2  4300  0in  4377  disjr  4431  disjdifr  4453  difdifdir  4472  uneqdifeq  4473  disjtp2  4697  iinrab2  5051  iunin1  5053  iinin1  5060  riinn0  5064  disjprg  5120  disjxun  5122  inex2  5293  inex2g  5295  rescom  5994  resindm  6022  resdmdfsn  6023  resopab  6026  imadisj  6072  intirr  6112  djudisj  6161  imainrect  6175  dmresv  6194  resdmres  6226  coeq0  6249  dfpred3  6306  predres  6333  frpoind  6336  wfiOLD  6345  ordtri3or  6389  fnresdisj  6663  fnimaeq0  6676  resasplit  6753  fresaun  6754  fresaunres2  6755  fresaunres1  6756  f0rn0  6768  fvun2  6976  rescnvimafod  7068  fveqressseq  7074  ressnop0  7148  fninfp  7171  fsnunfv  7184  orduniss2  7832  offres  7987  curry1  8108  curry2  8111  fpar  8120  fprlem1  8304  wfrlem5OLD  8332  smores3  8372  oacomf1o  8582  domunsncan  9091  phplem2OLD  9234  dif1ennnALT  9288  domunfican  9338  marypha1lem  9450  zfregfr  9624  epfrs  9750  zfregs2  9752  frind  9769  frrlem15  9776  djuin  9937  tskwe  9969  dfac8b  10050  ac10ct  10053  kmlem11  10180  kmlem12  10181  djucomen  10197  onadju  10213  ackbij1lem14  10251  ackbij1lem16  10253  fin23lem26  10344  fin23lem19  10355  fin23lem30  10361  isf32lem4  10375  isf34lem7  10398  isf34lem6  10399  axdc3lem4  10472  brdom7disj  10550  brdom6disj  10551  fpwwe2lem12  10661  fzpreddisj  13595  fzdifsuc  13606  fseq1p1m1  13620  prinfzo0  13720  hashun3  14407  hashbclem  14475  hash7g  14509  xpcoidgend  14999  cotr2  15001  limsupgle  15498  prmreclem2  16942  setsdm  17194  ressinbas  17271  wunress  17275  mreexexlem2d  17662  oppcinv  17798  cnvps  18593  pmtrmvd  19442  lsmmod2  19662  lsmdisj3  19669  lsmdisjr  19670  lsmdisj2r  19671  lsmdisj3r  19672  lsmdisj2a  19673  lsmdisj2b  19674  lsmdisj3a  19675  lsmdisj3b  19676  subgdisj2  19678  pj2f  19684  pj1id  19685  frgpuplem  19758  gsummptfzsplitl  19919  dprd2da  20030  dmdprdsplit2lem  20033  dmdprdsplit2  20034  pgpfaclem1  20069  rnghmsscmap2  20594  rnghmsubcsetclem1  20596  rnghmsubcsetc  20598  rngccat  20599  rngcid  20600  rngcifuestrc  20604  funcrngcsetc  20605  rhmsscmap2  20623  rhmsubcsetclem1  20625  rhmsubcsetc  20627  ringccat  20628  ringcid  20629  rhmsscrnghm  20630  rhmsubcrngclem1  20631  rhmsubcrngc  20633  rngcresringcat  20634  funcringcsetc  20639  rngcrescrhm  20649  rhmsubclem3  20652  rhmsubc  20654  lmhmlsp  21012  psgndiflemB  21565  pjpm  21673  ltbwe  22007  psrbag0  22025  elcls  23016  mretopd  23035  restin  23109  restcld  23115  resstopn  23129  lecldbas  23162  nrmsep  23300  isreg2  23320  ordthaus  23327  cmpsublem  23342  cmpsub  23343  hauscmplem  23349  bwth  23353  iunconn  23371  cldllycmp  23438  kgentopon  23481  llycmpkgen2  23493  1stckgen  23497  txkgen  23595  kqcldsat  23676  regr1lem2  23683  fbun  23783  fin1aufil  23875  fclsfnflim  23970  ustexsym  24159  restutopopn  24182  ustuqtop5  24189  ressuss  24206  metreslem  24306  blcld  24449  ressxms  24469  ressms  24470  reconn  24773  metdseq0  24799  metnrmlem3  24806  unmbl  25495  volun  25503  iundisj2  25507  icombl  25522  ioombl  25523  uniioombllem2  25541  uniioombllem4  25544  dyaddisjlem  25553  dyaddisj  25554  mbfconstlem  25585  mbfeqalem2  25600  ismbf3d  25612  itg1addlem5  25658  itgsplitioo  25796  lhop  25978  vieta1lem2  26276  xrlimcnp  26935  perfectlem2  27198  rplogsum  27495  nosupbnd2lem1  27684  sltlpss  27876  slelss  27877  perpcom  28697  vtxdgoddnumeven  29538  ex-dif  30409  ococi  31391  orthin  31432  lediri  31523  pjoml2i  31571  pjoml4i  31573  cmcmlem  31577  cmbr3i  31586  cmm2i  31593  cm0  31595  fh1  31604  fh2  31605  cm2j  31606  qlaxr3i  31622  pjclem2  32182  stm1ri  32230  golem1  32257  dmdbr5  32294  mddmd2  32295  cvmdi  32310  mdsldmd1i  32317  csmdsymi  32320  mdexchi  32321  cvexchi  32355  atssma  32364  atomli  32368  atoml2i  32369  atordi  32370  atcvatlem  32371  chirredlem1  32376  chirredlem2  32377  chirredlem3  32378  atcvat4i  32383  atabsi  32387  mdsymlem1  32389  dmdbr6ati  32409  cdj3lem3  32424  inin  32502  difuncomp  32539  iundisj2f  32576  disjunsn  32580  imadifxp  32587  fnresin  32609  mptiffisupp  32675  mptprop  32680  df1stres  32686  df2ndres  32687  padct  32702  iocinif  32763  difioo  32764  fzodif1  32774  iundisj2fi  32779  xrge00  33012  symgcom  33099  cycpm2tr  33135  cycpmco2f1  33140  xrge0slmod  33368  ssdifidlprm  33478  oppr2idl  33506  ufdprmidl  33561  1arithufdlem4  33567  lindsun  33670  fldexttr  33705  lmxrge0  33988  esumrnmpt2  34104  esumpfinvallem  34110  ldgenpisyslem1  34199  ldgenpisys  34202  measxun2  34246  measunl  34252  carsgclctunlem1  34354  carsgclctunlem2  34356  eulerpartlemt  34408  eulerpartgbij  34409  probmeasb  34467  bayesth  34476  ballotlemfp1  34529  ballotlemfval0  34533  signstres  34612  hashreprin  34657  reprfz1  34661  chtvalz  34666  breprexpnat  34671  f1resrcmplf1d  35123  f1resfz0f1d  35141  subfacp1lem3  35209  subfacp1lem5  35211  pconnconn  35258  cvmscld  35300  cvmsss2  35301  satef  35443  satefvfmla0  35445  mrsubvrs  35549  cldbnd  36349  bj-inrab3  36952  bj-2upln1upl  37047  bj-sscon  37052  bj-rest0  37116  bj-0int  37124  bj-ismooredr2  37133  icoreclin  37380  fin2so  37636  ptrest  37648  poimirlem3  37652  poimirlem11  37660  poimirlem12  37661  poimirlem13  37662  poimirlem14  37663  poimirlem15  37664  poimirlem18  37667  poimirlem21  37670  poimirlem22  37671  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  cnambfre  37697  asindmre  37732  dvasin  37733  dvreasin  37735  dvreacos  37736  sstotbnd2  37803  bndss  37815  inres2  38269  disjressuc2  38411  redundss3  38651  l1cvat  39078  pmod2iN  39873  pmodN  39874  pmodl42N  39875  osumcllem3N  39982  osumcllem4N  39983  dihmeetlem19N  41349  dihmeetALTN  41351  readvrec2  42379  elrfi  42692  diophrw  42757  eldioph2lem1  42758  eldioph2lem2  42759  diophin  42770  diophren  42811  dnwech  43047  fnwe2lem2  43050  kelac2lem  43063  kelac2  43064  lmhmlnmsplit  43086  pwssplit4  43088  pwfi2f1o  43095  proot1hash  43194  naddov4  43382  rp-fakeuninass  43515  elcnvcnvintab  43581  relintab  43582  elcnvcnvlem  43598  conrel1d  43662  dfrcl2  43673  iunrelexp0  43701  ntrk0kbimka  44038  hashnzfz  44319  zfregs2VD  44840  iunconnlem2  44934  ssinss2d  45064  restuni4  45125  restuni6  45126  restsubel  45157  iccdifioo  45524  uzinico2  45570  sumnnodd  45639  limsupvaluz  45717  cncfuni  45895  fouriersw  46240  saliinclf  46335  iundjiunlem  46468  iundjiun  46469  caragenuncllem  46521  caragendifcl  46523  hoidmvlelem2  46605  smflimlem1  46780  3f1oss1  47084  perfectALTVlem2  47716  rngchomrnghmresALTV  48234  rngcrescrhmALTV  48235  rhmsubcALTVlem3  48238  rhmsubcALTVlem4  48239  resinsn  48827  resinsnALT  48828  tposrescnv  48834  opndisj  48857  restclssep  48870  seposep  48880  iscnrm3rlem3  48896  iscnrm3rlem8  48901  oppczeroo  49134