Theorem incom 4178

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  {crab 3142   ∩ cin 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-rab 3147  df-in 3943

This theorem is referenced by:  ineq2  4183  sseqin2  4192  in12  4197  in32  4198  in13  4199  in31  4200  inss2  4206  sslin  4211  inss  4215  dfss7  4217  indif1  4248  indifcom  4249  indir  4252  dfsymdif3  4269  dfrab2  4279  0in  4347  disjr  4400  ssdifin0  4431  difdifdir  4437  uneqdifeq  4438  disjtp2  4652  iinrab2  4992  iunin1  4994  iinin1  5001  riinn0  5005  disjprgw  5061  disjprg  5062  disjxun  5064  inex2  5222  inex2g  5224  rescom  5879  resindm  5900  resdmdfsn  5901  resopab  5902  imadisj  5948  intirr  5978  djudisj  6024  imainrect  6038  dmresv  6057  resdmres  6089  coeq0  6108  dfpred3  6158  wfi  6181  ordtri3or  6223  fnresdisj  6467  fnimaeq0  6481  resasplit  6548  fresaun  6549  fresaunres2  6550  fresaunres1  6551  f0rn0  6564  fvun2  6755  fveqressseq  6847  ressnop0  6915  fninfp  6936  fvsnun1  6944  fsnunfv  6949  fveqf1o  7058  orduniss2  7548  offres  7684  curry1  7799  curry2  7802  fpar  7811  wfrlem5  7959  smores3  7990  oacomf1o  8191  ralxpmap  8460  difsnen  8599  domunsncan  8617  domunsn  8667  limensuci  8693  phplem2  8697  pssnn  8736  dif1en  8751  domunfican  8791  marypha1lem  8897  zfregfr  9068  epfrs  9173  zfregs2  9175  djuin  9347  tskwe  9379  dif1card  9436  dfac8b  9457  ac10ct  9460  kmlem11  9586  kmlem12  9587  djucomen  9603  onadju  9619  ackbij1lem14  9655  ackbij1lem16  9657  ackbij1lem18  9659  fin23lem26  9747  fin23lem19  9758  fin23lem30  9764  isf32lem4  9778  isf34lem7  9801  isf34lem6  9802  axdc3lem4  9875  brdom7disj  9953  brdom6disj  9954  fpwwe2lem13  10064  canthp1lem1  10074  grothprim  10256  fzpreddisj  12957  fzdifsuc  12968  fseq1p1m1  12982  prinfzo0  13077  hashgval  13694  hashun3  13746  hashfun  13799  hashbclem  13811  xpcoidgend  14335  cotr2  14337  limsupgle  14834  prmreclem2  16253  setsdm  16517  setsfun  16518  setsfun0  16519  setsid  16538  ressinbas  16560  wunress  16564  mreexexlem2d  16916  mreexexlem4d  16918  oppcinv  17050  cnvps  17822  pmtrmvd  18584  lsmmod2  18802  lsmdisj3  18809  lsmdisjr  18810  lsmdisj2r  18811  lsmdisj3r  18812  lsmdisj2a  18813  lsmdisj2b  18814  lsmdisj3a  18815  lsmdisj3b  18816  subgdisj2  18818  pj2f  18824  pj1id  18825  frgpuplem  18898  gsummptfzsplitl  19053  dprd2da  19164  dmdprdsplit2lem  19167  dmdprdsplit2  19168  pgpfaclem1  19203  lmhmlsp  19821  pwssplit1  19831  ltbwe  20253  psrbag0  20274  cnfldfun  20557  psgndiflemB  20744  pjpm  20852  islindf4  20982  elcls  21681  mretopd  21700  restin  21774  restcld  21780  neitr  21788  resstopn  21794  lecldbas  21827  nrmsep  21965  regsep2  21984  isreg2  21985  ordthaus  21992  cmpsublem  22007  cmpsub  22008  hauscmplem  22014  bwth  22018  iunconn  22036  cldllycmp  22103  kgentopon  22146  llycmpkgen2  22158  1stckgen  22162  txkgen  22260  kqcldsat  22341  regr1lem2  22348  fbun  22448  fin1aufil  22540  fclsfnflim  22635  ustexsym  22824  restutopopn  22847  ustuqtop5  22854  ressuss  22872  metreslem  22972  blcld  23115  ressxms  23135  ressms  23136  restmetu  23180  reconn  23436  metdseq0  23462  metnrmlem3  23469  unmbl  24138  volun  24146  volinun  24147  iundisj2  24150  icombl  24165  ioombl  24166  uniioombllem2  24184  uniioombllem4  24187  dyaddisjlem  24196  dyaddisj  24197  mbfconstlem  24228  mbfeqalem2  24243  ismbf3d  24255  itg1addlem5  24301  itgsplitioo  24438  lhop  24613  tdeglem4  24654  vieta1lem2  24900  xrlimcnp  25546  perfectlem2  25806  rplogsum  26103  perpcom  26499  vtxdgoddnumeven  27335  ex-dif  28202  ococi  29182  orthin  29223  lediri  29314  pjoml2i  29362  pjoml4i  29364  cmcmlem  29368  cmbr3i  29377  cmm2i  29384  cm0  29386  fh1  29395  fh2  29396  cm2j  29397  qlaxr3i  29413  pjclem2  29973  stm1ri  30021  golem1  30048  dmdbr5  30085  mddmd2  30086  cvmdi  30101  mdsldmd1i  30108  csmdsymi  30111  mdexchi  30112  cvexchi  30146  atssma  30155  atomli  30159  atoml2i  30160  atordi  30161  atcvatlem  30162  chirredlem1  30167  chirredlem2  30168  chirredlem3  30169  atcvat4i  30174  atabsi  30178  mdsymlem1  30180  dmdbr6ati  30200  cdj3lem3  30215  disjdifr  30275  inin  30277  difeq  30280  difuncomp  30305  disjdifprg  30325  iundisj2f  30340  disjunsn  30344  imadifxp  30351  fnresin  30371  fnunres2  30424  mptprop  30434  df1stres  30439  df2ndres  30440  padct  30455  iocinif  30504  difioo  30505  fzodif1  30516  iundisj2fi  30520  xrge00  30673  symgcom  30727  tocycfvres1  30752  tocycfvres2  30753  cycpmfvlem  30754  cycpmfv3  30757  cycpmcl  30758  cycpm2tr  30761  cycpmco2f1  30766  xrge0slmod  30917  lindsun  31021  fldexttr  31048  lmxrge0  31195  esumrnmpt2  31327  esumpfinvallem  31333  ldgenpisyslem1  31422  ldgenpisys  31425  measxun2  31469  measunl  31475  carsgclctunlem1  31575  carsgclctunlem2  31577  eulerpartlemt  31629  eulerpartgbij  31630  probmeasb  31688  bayesth  31697  ballotlemfp1  31749  ballotlemfval0  31753  signstres  31845  hashreprin  31891  reprfz1  31895  chtvalz  31900  breprexpnat  31905  f1resrcmplf1d  32360  f1resfz0f1d  32361  subfacp1lem3  32429  subfacp1lem5  32431  pconnconn  32478  cvmscld  32520  cvmsss2  32521  satef  32663  satefvfmla0  32665  mrsubvrs  32769  mthmpps  32829  frpoind  33080  frind  33085  fprlem1  33137  frrlem15  33142  nosupbnd2lem1  33215  noetalem2  33218  noetalem3  33219  cldbnd  33674  bj-inrab3  34250  bj-2upln1upl  34339  bj-sscon  34344  bj-rest0  34387  bj-0int  34396  bj-ismooredr2  34405  icoreclin  34641  fin2so  34894  ptrest  34906  poimirlem3  34910  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem16  34923  poimirlem18  34925  poimirlem19  34926  poimirlem21  34928  poimirlem22  34929  poimirlem27  34934  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  cnambfre  34955  asindmre  34992  dvasin  34993  dvreasin  34995  dvreacos  34996  sstotbnd2  35067  bndss  35079  ineqcom  35519  inres2  35521  redundss3  35878  l1cvat  36206  pmod2iN  37000  pmodN  37001  pmodl42N  37002  osumcllem3N  37109  osumcllem4N  37110  dihmeetlem19N  38476  dihmeetALTN  38478  elrfi  39340  diophrw  39405  eldioph2lem1  39406  eldioph2lem2  39407  diophin  39418  diophren  39459  dnwech  39697  fnwe2lem2  39700  kelac1  39712  kelac2lem  39713  kelac2  39714  lmhmlnmsplit  39736  pwssplit4  39738  pwfi2f1o  39745  proot1hash  39849  rp-fakeuninass  39931  elcnvcnvintab  39991  relintab  39992  elcnvcnvlem  40008  conrel1d  40057  dfrcl2  40068  iunrelexp0  40096  ntrk0kbimka  40438  hashnzfz  40701  zfregs2VD  41224  iunconnlem2  41318  ssinss2d  41371  restuni4  41436  restuni6  41437  iccdifioo  41840  uzinico2  41887  sumnnodd  41960  limsupvaluz  42038  cncfuni  42218  fouriersw  42565  saliincl  42659  iundjiunlem  42790  iundjiun  42791  caragenuncllem  42843  caragendifcl  42845  isomenndlem  42861  hoidmvlelem2  42927  smflimlem1  43096  perfectALTVlem2  43936  rnghmsscmap2  44293  rnghmsubcsetclem1  44295  rnghmsubcsetc  44297  rngccat  44298  rngcid  44299  rngchomrnghmresALTV  44316  rngcifuestrc  44317  funcrngcsetc  44318  rhmsscmap2  44339  rhmsubcsetclem1  44341  rhmsubcsetc  44343  ringccat  44344  ringcid  44345  rhmsscrnghm  44346  rhmsubcrngclem1  44347  rhmsubcrngc  44349  rngcresringcat  44350  funcringcsetc  44355  rngcrescrhm  44405  rhmsubclem3  44408  rhmsubc  44410  rngcrescrhmALTV  44423  rhmsubcALTVlem3  44426  rhmsubcALTVlem4  44427