Theorem incom 4193

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  {crab 3424   ∩ cin 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-rab 3425  df-in 3947

This theorem is referenced by:  ineqcom  4194  ineqcomi  4195  ineq2  4198  sseqin2  4207  in12  4212  in32  4213  in13  4214  in31  4215  inss2  4221  sslin  4226  inss  4230  dfss7  4232  indif1  4263  indifcom  4264  indir  4267  indifdir  4276  dfsymdif3  4288  dfrab2  4302  0in  4385  disjr  4441  disjdifr  4464  difdifdir  4483  uneqdifeq  4484  disjtp2  4712  iinrab2  5063  iunin1  5065  iinin1  5072  riinn0  5076  disjprgw  5133  disjprg  5134  disjxun  5136  inex2  5308  inex2g  5310  rescom  5997  resindm  6020  resdmdfsn  6021  resopab  6024  imadisj  6069  intirr  6109  djudisj  6156  imainrect  6170  dmresv  6189  resdmres  6221  coeq0  6244  dfpred3  6301  predres  6330  frpoind  6333  wfiOLD  6342  ordtri3or  6386  fnresdisj  6660  fnimaeq0  6673  resasplit  6751  fresaun  6752  fresaunres2  6753  fresaunres1  6754  f0rn0  6766  fvun2  6973  rescnvimafod  7065  fveqressseq  7071  ressnop0  7143  fninfp  7164  fsnunfv  7177  orduniss2  7814  offres  7963  curry1  8084  curry2  8087  fpar  8096  fprlem1  8280  wfrlem5OLD  8308  smores3  8348  oacomf1o  8560  domunsncan  9067  phplem2OLD  9213  pssnnOLD  9260  dif1ennnALT  9272  domunfican  9315  marypha1lem  9423  zfregfr  9595  epfrs  9721  zfregs2  9723  frind  9740  frrlem15  9747  djuin  9908  tskwe  9940  dfac8b  10021  ac10ct  10024  kmlem11  10150  kmlem12  10151  djucomen  10167  onadju  10183  ackbij1lem14  10223  ackbij1lem16  10225  fin23lem26  10315  fin23lem19  10326  fin23lem30  10332  isf32lem4  10346  isf34lem7  10369  isf34lem6  10370  axdc3lem4  10443  brdom7disj  10521  brdom6disj  10522  fpwwe2lem12  10632  fzpreddisj  13546  fzdifsuc  13557  fseq1p1m1  13571  prinfzo0  13667  hashun3  14340  hashbclem  14407  xpcoidgend  14918  cotr2  14920  limsupgle  15417  prmreclem2  16846  setsdm  17099  ressinbas  17186  wunress  17191  wunressOLD  17192  mreexexlem2d  17585  oppcinv  17723  cnvps  18530  pmtrmvd  19361  lsmmod2  19581  lsmdisj3  19588  lsmdisjr  19589  lsmdisj2r  19590  lsmdisj3r  19591  lsmdisj2a  19592  lsmdisj2b  19593  lsmdisj3a  19594  lsmdisj3b  19595  subgdisj2  19597  pj2f  19603  pj1id  19604  frgpuplem  19677  gsummptfzsplitl  19838  dprd2da  19949  dmdprdsplit2lem  19952  dmdprdsplit2  19953  pgpfaclem1  19988  rnghmsscmap2  20510  rnghmsubcsetclem1  20512  rnghmsubcsetc  20514  rngccat  20515  rngcid  20516  rngcifuestrc  20520  funcrngcsetc  20521  rhmsscmap2  20539  rhmsubcsetclem1  20541  rhmsubcsetc  20543  ringccat  20544  ringcid  20545  rhmsscrnghm  20546  rhmsubcrngclem1  20547  rhmsubcrngc  20549  rngcresringcat  20550  funcringcsetc  20555  rngcrescrhm  20565  rhmsubclem3  20568  rhmsubc  20570  lmhmlsp  20882  cnfldfunALTOLD  21237  psgndiflemB  21453  pjpm  21563  ltbwe  21900  psrbag0  21924  elcls  22887  mretopd  22906  restin  22980  restcld  22986  resstopn  23000  lecldbas  23033  nrmsep  23171  isreg2  23191  ordthaus  23198  cmpsublem  23213  cmpsub  23214  hauscmplem  23220  bwth  23224  iunconn  23242  cldllycmp  23309  kgentopon  23352  llycmpkgen2  23364  1stckgen  23368  txkgen  23466  kqcldsat  23547  regr1lem2  23554  fbun  23654  fin1aufil  23746  fclsfnflim  23841  ustexsym  24030  restutopopn  24053  ustuqtop5  24060  ressuss  24077  metreslem  24178  blcld  24324  ressxms  24344  ressms  24345  reconn  24654  metdseq0  24680  metnrmlem3  24687  unmbl  25376  volun  25384  iundisj2  25388  icombl  25403  ioombl  25404  uniioombllem2  25422  uniioombllem4  25425  dyaddisjlem  25434  dyaddisj  25435  mbfconstlem  25466  mbfeqalem2  25481  ismbf3d  25493  itg1addlem5  25540  itgsplitioo  25677  lhop  25859  tdeglem4OLD  25906  vieta1lem2  26153  xrlimcnp  26804  perfectlem2  27067  rplogsum  27364  nosupbnd2lem1  27552  sltlpss  27737  slelss  27738  perpcom  28388  vtxdgoddnumeven  29234  ex-dif  30100  ococi  31082  orthin  31123  lediri  31214  pjoml2i  31262  pjoml4i  31264  cmcmlem  31268  cmbr3i  31277  cmm2i  31284  cm0  31286  fh1  31295  fh2  31296  cm2j  31297  qlaxr3i  31313  pjclem2  31873  stm1ri  31921  golem1  31948  dmdbr5  31985  mddmd2  31986  cvmdi  32001  mdsldmd1i  32008  csmdsymi  32011  mdexchi  32012  cvexchi  32046  atssma  32055  atomli  32059  atoml2i  32060  atordi  32061  atcvatlem  32062  chirredlem1  32067  chirredlem2  32068  chirredlem3  32069  atcvat4i  32074  atabsi  32078  mdsymlem1  32080  dmdbr6ati  32100  cdj3lem3  32115  inin  32177  difuncomp  32209  iundisj2f  32245  disjunsn  32249  imadifxp  32256  fnresin  32274  mptiffisupp  32339  mptprop  32344  df1stres  32349  df2ndres  32350  padct  32368  iocinif  32416  difioo  32417  fzodif1  32428  iundisj2fi  32432  xrge00  32611  symgcom  32671  cycpm2tr  32705  cycpmco2f1  32710  xrge0slmod  32890  oppr2idl  33031  lindsun  33155  fldexttr  33182  lmxrge0  33387  esumrnmpt2  33521  esumpfinvallem  33527  ldgenpisyslem1  33616  ldgenpisys  33619  measxun2  33663  measunl  33669  carsgclctunlem1  33771  carsgclctunlem2  33773  eulerpartlemt  33825  eulerpartgbij  33826  probmeasb  33884  bayesth  33893  ballotlemfp1  33945  ballotlemfval0  33949  signstres  34041  hashreprin  34087  reprfz1  34091  chtvalz  34096  breprexpnat  34101  f1resrcmplf1d  34545  f1resfz0f1d  34558  subfacp1lem3  34628  subfacp1lem5  34630  pconnconn  34677  cvmscld  34719  cvmsss2  34720  satef  34862  satefvfmla0  34864  mrsubvrs  34968  cldbnd  35667  bj-inrab3  36265  bj-2upln1upl  36361  bj-sscon  36366  bj-rest0  36430  bj-0int  36438  bj-ismooredr2  36447  icoreclin  36694  fin2so  36931  ptrest  36943  poimirlem3  36947  poimirlem11  36955  poimirlem12  36956  poimirlem13  36957  poimirlem14  36958  poimirlem15  36959  poimirlem18  36962  poimirlem21  36965  poimirlem22  36966  mblfinlem3  36983  mblfinlem4  36984  ismblfin  36985  cnambfre  36992  asindmre  37027  dvasin  37028  dvreasin  37030  dvreacos  37031  sstotbnd2  37098  bndss  37110  inres2  37568  disjressuc2  37714  redundss3  37954  l1cvat  38381  pmod2iN  39176  pmodN  39177  pmodl42N  39178  osumcllem3N  39285  osumcllem4N  39286  dihmeetlem19N  40652  dihmeetALTN  40654  metakunt18  41461  elrfi  41887  diophrw  41952  eldioph2lem1  41953  eldioph2lem2  41954  diophin  41965  diophren  42006  dnwech  42245  fnwe2lem2  42248  kelac2lem  42261  kelac2  42262  lmhmlnmsplit  42284  pwssplit4  42286  pwfi2f1o  42293  proot1hash  42397  naddov4  42588  rp-fakeuninass  42722  elcnvcnvintab  42788  relintab  42789  elcnvcnvlem  42805  conrel1d  42869  dfrcl2  42880  iunrelexp0  42908  ntrk0kbimka  43245  hashnzfz  43534  zfregs2VD  44057  iunconnlem2  44151  ssinss2d  44201  restuni4  44264  restuni6  44265  restsubel  44301  iccdifioo  44679  uzinico2  44726  sumnnodd  44797  limsupvaluz  44875  cncfuni  45053  fouriersw  45398  saliinclf  45493  iundjiunlem  45626  iundjiun  45627  caragenuncllem  45679  caragendifcl  45681  hoidmvlelem2  45763  smflimlem1  45938  perfectALTVlem2  46841  rngchomrnghmresALTV  47108  rngcrescrhmALTV  47109  rhmsubcALTVlem3  47112  rhmsubcALTVlem4  47113  opndisj  47689  restclssep  47702  seposep  47712  iscnrm3rlem3  47729  iscnrm3rlem8  47734