Theorem incom 4176

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

Syntax hints:   = wceq 1531   ∈ wcel 2108  {crab 3140   ∩ cin 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1534  df-ex 1775  df-sb 2064  df-clab 2798  df-cleq 2812  df-rab 3145  df-in 3941

This theorem is referenced by:  ineq2  4181  sseqin2  4190  in12  4195  in32  4196  in13  4197  in31  4198  inss2  4204  sslin  4209  inss  4213  dfss7  4215  indif1  4246  indifcom  4247  indir  4250  dfsymdif3  4267  dfrab2  4277  0in  4345  disjr  4398  ssdifin0  4429  difdifdir  4435  uneqdifeq  4436  disjtp2  4644  iinrab2  4983  iunin1  4985  iinin1  4992  riinn0  4996  disjprgw  5052  disjprg  5053  disjxun  5055  inex2  5213  inex2g  5215  rescom  5872  resindm  5893  resdmdfsn  5894  resopab  5895  imadisj  5941  intirr  5971  djudisj  6017  imainrect  6031  dmresv  6050  resdmres  6082  coeq0  6101  dfpred3  6151  wfi  6174  ordtri3or  6216  fnresdisj  6460  fnimaeq0  6474  resasplit  6541  fresaun  6542  fresaunres2  6543  fresaunres1  6544  f0rn0  6557  fvun2  6748  fveqressseq  6840  ressnop0  6908  fninfp  6929  fvsnun1  6937  fsnunfv  6942  fveqf1o  7050  orduniss2  7540  offres  7676  curry1  7791  curry2  7794  fpar  7803  wfrlem5  7951  smores3  7982  oacomf1o  8183  ralxpmap  8452  difsnen  8591  domunsncan  8609  domunsn  8659  limensuci  8685  phplem2  8689  pssnn  8728  dif1en  8743  domunfican  8783  marypha1lem  8889  zfregfr  9060  epfrs  9165  zfregs2  9167  djuin  9339  tskwe  9371  dif1card  9428  dfac8b  9449  ac10ct  9452  kmlem11  9578  kmlem12  9579  djucomen  9595  onadju  9611  ackbij1lem14  9647  ackbij1lem16  9649  ackbij1lem18  9651  fin23lem26  9739  fin23lem19  9750  fin23lem30  9756  isf32lem4  9770  isf34lem7  9793  isf34lem6  9794  axdc3lem4  9867  brdom7disj  9945  brdom6disj  9946  fpwwe2lem13  10056  canthp1lem1  10066  grothprim  10248  fzpreddisj  12948  fzdifsuc  12959  fseq1p1m1  12973  prinfzo0  13068  hashgval  13685  hashun3  13737  hashfun  13790  hashbclem  13802  xpcoidgend  14327  cotr2  14329  limsupgle  14826  prmreclem2  16245  setsdm  16509  setsfun  16510  setsfun0  16511  setsid  16530  ressinbas  16552  wunress  16556  mreexexlem2d  16908  mreexexlem4d  16910  oppcinv  17042  cnvps  17814  pmtrmvd  18576  lsmmod2  18794  lsmdisj3  18801  lsmdisjr  18802  lsmdisj2r  18803  lsmdisj3r  18804  lsmdisj2a  18805  lsmdisj2b  18806  lsmdisj3a  18807  lsmdisj3b  18808  subgdisj2  18810  pj2f  18816  pj1id  18817  frgpuplem  18890  gsummptfzsplitl  19045  dprd2da  19156  dmdprdsplit2lem  19159  dmdprdsplit2  19160  pgpfaclem1  19195  lmhmlsp  19813  pwssplit1  19823  ltbwe  20245  psrbag0  20266  cnfldfun  20549  psgndiflemB  20736  pjpm  20844  islindf4  20974  elcls  21673  mretopd  21692  restin  21766  restcld  21772  neitr  21780  resstopn  21786  lecldbas  21819  nrmsep  21957  regsep2  21976  isreg2  21977  ordthaus  21984  cmpsublem  21999  cmpsub  22000  hauscmplem  22006  bwth  22010  iunconn  22028  cldllycmp  22095  kgentopon  22138  llycmpkgen2  22150  1stckgen  22154  txkgen  22252  kqcldsat  22333  regr1lem2  22340  fbun  22440  fin1aufil  22532  fclsfnflim  22627  ustexsym  22816  restutopopn  22839  ustuqtop5  22846  ressuss  22864  metreslem  22964  blcld  23107  ressxms  23127  ressms  23128  restmetu  23172  reconn  23428  metdseq0  23454  metnrmlem3  23461  unmbl  24130  volun  24138  volinun  24139  iundisj2  24142  icombl  24157  ioombl  24158  uniioombllem2  24176  uniioombllem4  24179  dyaddisjlem  24188  dyaddisj  24189  mbfconstlem  24220  mbfeqalem2  24235  ismbf3d  24247  itg1addlem5  24293  itgsplitioo  24430  lhop  24605  tdeglem4  24646  vieta1lem2  24892  xrlimcnp  25538  perfectlem2  25798  rplogsum  26095  perpcom  26491  vtxdgoddnumeven  27327  ex-dif  28194  ococi  29174  orthin  29215  lediri  29306  pjoml2i  29354  pjoml4i  29356  cmcmlem  29360  cmbr3i  29369  cmm2i  29376  cm0  29378  fh1  29387  fh2  29388  cm2j  29389  qlaxr3i  29405  pjclem2  29965  stm1ri  30013  golem1  30040  dmdbr5  30077  mddmd2  30078  cvmdi  30093  mdsldmd1i  30100  csmdsymi  30103  mdexchi  30104  cvexchi  30138  atssma  30147  atomli  30151  atoml2i  30152  atordi  30153  atcvatlem  30154  chirredlem1  30159  chirredlem2  30160  chirredlem3  30161  atcvat4i  30166  atabsi  30170  mdsymlem1  30172  dmdbr6ati  30192  cdj3lem3  30207  disjdifr  30267  inin  30269  difeq  30272  difuncomp  30297  disjdifprg  30317  iundisj2f  30332  disjunsn  30336  imadifxp  30343  fnresin  30363  fnunres2  30416  mptprop  30426  df1stres  30431  df2ndres  30432  padct  30447  iocinif  30496  difioo  30497  fzodif1  30508  iundisj2fi  30512  xrge00  30666  symgcom  30720  tocycfvres1  30745  tocycfvres2  30746  cycpmfvlem  30747  cycpmfv3  30750  cycpmcl  30751  cycpm2tr  30754  cycpmco2f1  30759  xrge0slmod  30910  lindsun  31014  fldexttr  31041  lmxrge0  31188  esumrnmpt2  31320  esumpfinvallem  31326  ldgenpisyslem1  31415  ldgenpisys  31418  measxun2  31462  measunl  31468  carsgclctunlem1  31568  carsgclctunlem2  31570  eulerpartlemt  31622  eulerpartgbij  31623  probmeasb  31681  bayesth  31690  ballotlemfp1  31742  ballotlemfval0  31746  signstres  31838  hashreprin  31884  reprfz1  31888  chtvalz  31893  breprexpnat  31898  f1resrcmplf1d  32353  f1resfz0f1d  32354  subfacp1lem3  32422  subfacp1lem5  32424  pconnconn  32471  cvmscld  32513  cvmsss2  32514  satef  32656  satefvfmla0  32658  mrsubvrs  32762  mthmpps  32822  frpoind  33073  frind  33078  fprlem1  33130  frrlem15  33135  nosupbnd2lem1  33208  noetalem2  33211  noetalem3  33212  cldbnd  33667  bj-inrab3  34240  bj-2upln1upl  34329  bj-sscon  34334  bj-rest0  34376  bj-0int  34385  bj-ismooredr2  34394  icoreclin  34630  fin2so  34871  ptrest  34883  poimirlem3  34887  poimirlem11  34895  poimirlem12  34896  poimirlem13  34897  poimirlem14  34898  poimirlem15  34899  poimirlem16  34900  poimirlem18  34902  poimirlem19  34903  poimirlem21  34905  poimirlem22  34906  poimirlem27  34911  mblfinlem3  34923  mblfinlem4  34924  ismblfin  34925  cnambfre  34932  asindmre  34969  dvasin  34970  dvreasin  34972  dvreacos  34973  sstotbnd2  35044  bndss  35056  ineqcom  35496  inres2  35498  redundss3  35855  l1cvat  36183  pmod2iN  36977  pmodN  36978  pmodl42N  36979  osumcllem3N  37086  osumcllem4N  37087  dihmeetlem19N  38453  dihmeetALTN  38455  elrfi  39281  diophrw  39346  eldioph2lem1  39347  eldioph2lem2  39348  diophin  39359  diophren  39400  dnwech  39638  fnwe2lem2  39641  kelac1  39653  kelac2lem  39654  kelac2  39655  lmhmlnmsplit  39677  pwssplit4  39679  pwfi2f1o  39686  proot1hash  39790  rp-fakeuninass  39872  elcnvcnvintab  39932  relintab  39933  elcnvcnvlem  39949  conrel1d  39998  dfrcl2  40009  iunrelexp0  40037  ntrk0kbimka  40379  hashnzfz  40642  zfregs2VD  41165  iunconnlem2  41259  ssinss2d  41312  restuni4  41377  restuni6  41378  iccdifioo  41780  uzinico2  41827  sumnnodd  41900  limsupvaluz  41978  cncfuni  42158  fouriersw  42506  saliincl  42600  iundjiunlem  42731  iundjiun  42732  caragenuncllem  42784  caragendifcl  42786  isomenndlem  42802  hoidmvlelem2  42868  smflimlem1  43037  perfectALTVlem2  43877  rnghmsscmap2  44234  rnghmsubcsetclem1  44236  rnghmsubcsetc  44238  rngccat  44239  rngcid  44240  rngchomrnghmresALTV  44257  rngcifuestrc  44258  funcrngcsetc  44259  rhmsscmap2  44280  rhmsubcsetclem1  44282  rhmsubcsetc  44284  ringccat  44285  ringcid  44286  rhmsscrnghm  44287  rhmsubcrngclem1  44288  rhmsubcrngc  44290  rngcresringcat  44291  funcringcsetc  44296  rngcrescrhm  44346  rhmsubclem3  44349  rhmsubc  44351  rngcrescrhmALTV  44364  rhmsubcALTVlem3  44367  rhmsubcALTVlem4  44368