Theorem incom 4156

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  {crab 3395   ∩ cin 3896

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 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-rab 3396  df-in 3904

This theorem is referenced by:  ineqcom  4157  ineqcomi  4158  ineq2  4161  sseqin2  4170  in12  4176  in32  4177  in13  4178  in31  4179  inss2  4185  sslin  4190  inss  4195  dfss7  4198  indif1  4229  indifcom  4230  indir  4233  indifdir  4242  dfsymdif3  4253  dfrab2  4267  0in  4344  disjr  4398  disjdifr  4420  difdifdir  4439  uneqdifeq  4440  disjtp2  4666  iinrab2  5016  iunin1  5018  iinin1  5025  riinn0  5029  disjprg  5085  disjxun  5087  inex2  5254  inex2g  5256  rescom  5950  resindm  5978  resdmdfsn  5979  resopab  5982  imadisj  6028  intirr  6064  djudisj  6114  imainrect  6128  dmresv  6147  resdmres  6179  coeq0  6203  dfpred3  6259  predres  6286  frpoind  6289  ordtri3or  6338  fnresdisj  6601  fnimaeq0  6614  resasplit  6693  fresaun  6694  fresaunres2  6695  fresaunres1  6696  f0rn0  6708  fvun2  6914  rescnvimafod  7006  fveqressseq  7012  ressnop0  7086  fninfp  7108  fsnunfv  7121  orduniss2  7763  offres  7915  curry1  8034  curry2  8037  fpar  8046  fprlem1  8230  smores3  8273  oacomf1o  8480  domunsncan  8990  dif1ennnALT  9161  domunfican  9206  marypha1lem  9317  zfregfr  9494  epfrs  9621  zfregs2  9623  frind  9643  frrlem15  9650  djuin  9811  tskwe  9843  dfac8b  9922  ac10ct  9925  kmlem11  10052  kmlem12  10053  djucomen  10069  onadju  10085  ackbij1lem14  10123  ackbij1lem16  10125  fin23lem26  10216  fin23lem19  10227  fin23lem30  10233  isf32lem4  10247  isf34lem7  10270  isf34lem6  10271  axdc3lem4  10344  brdom7disj  10422  brdom6disj  10423  fpwwe2lem12  10533  fzpreddisj  13473  fzdifsuc  13484  fseq1p1m1  13498  prinfzo0  13598  hashun3  14291  hashbclem  14359  hash7g  14393  xpcoidgend  14882  cotr2  14884  limsupgle  15384  prmreclem2  16829  setsdm  17081  ressinbas  17156  wunress  17160  mreexexlem2d  17551  oppcinv  17687  cnvps  18484  pmtrmvd  19368  lsmmod2  19588  lsmdisj3  19595  lsmdisjr  19596  lsmdisj2r  19597  lsmdisj3r  19598  lsmdisj2a  19599  lsmdisj2b  19600  lsmdisj3a  19601  lsmdisj3b  19602  subgdisj2  19604  pj2f  19610  pj1id  19611  frgpuplem  19684  gsummptfzsplitl  19845  dprd2da  19956  dmdprdsplit2lem  19959  dmdprdsplit2  19960  pgpfaclem1  19995  rnghmsscmap2  20544  rnghmsubcsetclem1  20546  rnghmsubcsetc  20548  rngccat  20549  rngcid  20550  rngcifuestrc  20554  funcrngcsetc  20555  rhmsscmap2  20573  rhmsubcsetclem1  20575  rhmsubcsetc  20577  ringccat  20578  ringcid  20579  rhmsscrnghm  20580  rhmsubcrngclem1  20581  rhmsubcrngc  20583  rngcresringcat  20584  funcringcsetc  20589  rngcrescrhm  20599  rhmsubclem3  20602  rhmsubc  20604  lmhmlsp  20983  psgndiflemB  21537  pjpm  21645  ltbwe  21979  psrbag0  21997  elcls  22988  mretopd  23007  restin  23081  restcld  23087  resstopn  23101  lecldbas  23134  nrmsep  23272  isreg2  23292  ordthaus  23299  cmpsublem  23314  cmpsub  23315  hauscmplem  23321  bwth  23325  iunconn  23343  cldllycmp  23410  kgentopon  23453  llycmpkgen2  23465  1stckgen  23469  txkgen  23567  kqcldsat  23648  regr1lem2  23655  fbun  23755  fin1aufil  23847  fclsfnflim  23942  ustexsym  24131  restutopopn  24153  ustuqtop5  24160  ressuss  24177  metreslem  24277  blcld  24420  ressxms  24440  ressms  24441  reconn  24744  metdseq0  24770  metnrmlem3  24777  unmbl  25465  volun  25473  iundisj2  25477  icombl  25492  ioombl  25493  uniioombllem2  25511  uniioombllem4  25514  dyaddisjlem  25523  dyaddisj  25524  mbfconstlem  25555  mbfeqalem2  25570  ismbf3d  25582  itg1addlem5  25628  itgsplitioo  25766  lhop  25948  vieta1lem2  26246  xrlimcnp  26905  perfectlem2  27168  rplogsum  27465  nosupbnd2lem1  27654  sltlpss  27853  slelss  27854  perpcom  28691  vtxdgoddnumeven  29532  ex-dif  30403  ococi  31385  orthin  31426  lediri  31517  pjoml2i  31565  pjoml4i  31567  cmcmlem  31571  cmbr3i  31580  cmm2i  31587  cm0  31589  fh1  31598  fh2  31599  cm2j  31600  qlaxr3i  31616  pjclem2  32176  stm1ri  32224  golem1  32251  dmdbr5  32288  mddmd2  32289  cvmdi  32304  mdsldmd1i  32311  csmdsymi  32314  mdexchi  32315  cvexchi  32349  atssma  32358  atomli  32362  atoml2i  32363  atordi  32364  atcvatlem  32365  chirredlem1  32370  chirredlem2  32371  chirredlem3  32372  atcvat4i  32377  atabsi  32381  mdsymlem1  32383  dmdbr6ati  32403  cdj3lem3  32418  inin  32496  difuncomp  32533  iundisj2f  32570  disjunsn  32574  imadifxp  32581  fnresin  32607  mptiffisupp  32674  mptprop  32679  df1stres  32685  df2ndres  32686  padct  32701  iocinif  32764  difioo  32765  fzodif1  32775  iundisj2fi  32779  xrge00  32995  symgcom  33052  cycpm2tr  33088  cycpmco2f1  33093  xrge0slmod  33313  ssdifidlprm  33423  oppr2idl  33451  ufdprmidl  33506  1arithufdlem4  33512  psrbasfsupp  33572  lindsun  33638  fldexttr  33671  lmxrge0  33965  esumrnmpt2  34081  esumpfinvallem  34087  ldgenpisyslem1  34176  ldgenpisys  34179  measxun2  34223  measunl  34229  carsgclctunlem1  34330  carsgclctunlem2  34332  eulerpartlemt  34384  eulerpartgbij  34385  probmeasb  34443  bayesth  34452  ballotlemfp1  34505  ballotlemfval0  34509  signstres  34588  hashreprin  34633  reprfz1  34637  chtvalz  34642  breprexpnat  34647  f1resrcmplf1d  35099  f1resfz0f1d  35158  subfacp1lem3  35226  subfacp1lem5  35228  pconnconn  35275  cvmscld  35317  cvmsss2  35318  satef  35460  satefvfmla0  35462  mrsubvrs  35566  cldbnd  36370  bj-inrab3  36973  bj-2upln1upl  37068  bj-sscon  37073  bj-rest0  37137  bj-0int  37145  bj-ismooredr2  37154  icoreclin  37401  fin2so  37657  ptrest  37669  poimirlem3  37673  poimirlem11  37681  poimirlem12  37682  poimirlem13  37683  poimirlem14  37684  poimirlem15  37685  poimirlem18  37688  poimirlem21  37691  poimirlem22  37692  mblfinlem3  37709  mblfinlem4  37710  ismblfin  37711  cnambfre  37718  asindmre  37753  dvasin  37754  dvreasin  37756  dvreacos  37757  sstotbnd2  37824  bndss  37836  inres2  38292  disjressuc2  38445  redundss3  38734  l1cvat  39164  pmod2iN  39958  pmodN  39959  pmodl42N  39960  osumcllem3N  40067  osumcllem4N  40068  dihmeetlem19N  41434  dihmeetALTN  41436  readvrec2  42464  elrfi  42797  diophrw  42862  eldioph2lem1  42863  eldioph2lem2  42864  diophin  42875  diophren  42916  dnwech  43151  fnwe2lem2  43154  kelac2lem  43167  kelac2  43168  lmhmlnmsplit  43190  pwssplit4  43192  pwfi2f1o  43199  proot1hash  43298  naddov4  43486  rp-fakeuninass  43619  elcnvcnvintab  43685  relintab  43686  elcnvcnvlem  43702  conrel1d  43766  dfrcl2  43777  iunrelexp0  43805  ntrk0kbimka  44142  hashnzfz  44423  zfregs2VD  44943  iunconnlem2  45037  ssinss2d  45167  restuni4  45228  restuni6  45229  restsubel  45260  iccdifioo  45625  uzinico2  45671  sumnnodd  45740  limsupvaluz  45816  cncfuni  45994  fouriersw  46339  saliinclf  46434  iundjiunlem  46567  iundjiun  46568  caragenuncllem  46620  caragendifcl  46622  hoidmvlelem2  46704  smflimlem1  46879  3f1oss1  47185  perfectALTVlem2  47832  rngchomrnghmresALTV  48389  rngcrescrhmALTV  48390  rhmsubcALTVlem3  48393  rhmsubcALTVlem4  48394  resinsn  48982  resinsnALT  48983  tposrescnv  48989  opndisj  49013  restclssep  49026  seposep  49036  iscnrm3rlem3  49052  iscnrm3rlem8  49057  oppczeroo  49348