Theorem incom 4135

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  {crab 3068   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-rab 3073  df-in 3894

This theorem is referenced by:  ineqcom  4136  ineqcomi  4137  ineq2  4140  sseqin2  4149  in12  4154  in32  4155  in13  4156  in31  4157  inss2  4163  sslin  4168  inss  4172  dfss7  4174  indif1  4205  indifcom  4206  indir  4209  indifdir  4218  dfsymdif3  4230  dfrab2  4244  0in  4327  disjr  4383  disjdifr  4406  difdifdir  4422  uneqdifeq  4423  disjtp2  4652  iinrab2  4999  iunin1  5001  iinin1  5008  riinn0  5012  disjprgw  5069  disjprg  5070  disjxun  5072  inex2  5242  inex2g  5244  rescom  5917  resindm  5940  resdmdfsn  5941  resopab  5942  imadisj  5988  intirr  6023  djudisj  6070  imainrect  6084  dmresv  6103  resdmres  6135  coeq0  6159  dfpred3  6213  predres  6242  frpoind  6245  wfiOLD  6254  ordtri3or  6298  fnresdisj  6552  fnimaeq0  6566  resasplit  6644  fresaun  6645  fresaunres2  6646  fresaunres1  6647  f0rn0  6659  fvun2  6860  rescnvimafod  6951  fveqressseq  6957  ressnop0  7025  fninfp  7046  fsnunfv  7059  orduniss2  7680  offres  7826  curry1  7944  curry2  7947  fpar  7956  fprlem1  8116  wfrlem5OLD  8144  smores3  8184  oacomf1o  8396  domunsncan  8859  phplem2OLD  9001  pssnnOLD  9040  dif1enALT  9050  domunfican  9087  marypha1lem  9192  zfregfr  9363  epfrs  9489  zfregs2  9491  frind  9508  frrlem15  9515  djuin  9676  tskwe  9708  dfac8b  9787  ac10ct  9790  kmlem11  9916  kmlem12  9917  djucomen  9933  onadju  9949  ackbij1lem14  9989  ackbij1lem16  9991  fin23lem26  10081  fin23lem19  10092  fin23lem30  10098  isf32lem4  10112  isf34lem7  10135  isf34lem6  10136  axdc3lem4  10209  brdom7disj  10287  brdom6disj  10288  fpwwe2lem12  10398  fzpreddisj  13305  fzdifsuc  13316  fseq1p1m1  13330  prinfzo0  13426  hashun3  14099  hashbclem  14164  xpcoidgend  14686  cotr2  14688  limsupgle  15186  prmreclem2  16618  setsdm  16871  ressinbas  16955  wunress  16960  wunressOLD  16961  mreexexlem2d  17354  oppcinv  17492  cnvps  18296  pmtrmvd  19064  lsmmod2  19282  lsmdisj3  19289  lsmdisjr  19290  lsmdisj2r  19291  lsmdisj3r  19292  lsmdisj2a  19293  lsmdisj2b  19294  lsmdisj3a  19295  lsmdisj3b  19296  subgdisj2  19298  pj2f  19304  pj1id  19305  frgpuplem  19378  gsummptfzsplitl  19534  dprd2da  19645  dmdprdsplit2lem  19648  dmdprdsplit2  19649  pgpfaclem1  19684  lmhmlsp  20311  cnfldfunALTOLD  20611  psgndiflemB  20805  pjpm  20915  ltbwe  21245  psrbag0  21270  elcls  22224  mretopd  22243  restin  22317  restcld  22323  resstopn  22337  lecldbas  22370  nrmsep  22508  isreg2  22528  ordthaus  22535  cmpsublem  22550  cmpsub  22551  hauscmplem  22557  bwth  22561  iunconn  22579  cldllycmp  22646  kgentopon  22689  llycmpkgen2  22701  1stckgen  22705  txkgen  22803  kqcldsat  22884  regr1lem2  22891  fbun  22991  fin1aufil  23083  fclsfnflim  23178  ustexsym  23367  restutopopn  23390  ustuqtop5  23397  ressuss  23414  metreslem  23515  blcld  23661  ressxms  23681  ressms  23682  reconn  23991  metdseq0  24017  metnrmlem3  24024  unmbl  24701  volun  24709  iundisj2  24713  icombl  24728  ioombl  24729  uniioombllem2  24747  uniioombllem4  24750  dyaddisjlem  24759  dyaddisj  24760  mbfconstlem  24791  mbfeqalem2  24806  ismbf3d  24818  itg1addlem5  24865  itgsplitioo  25002  lhop  25180  tdeglem4OLD  25225  vieta1lem2  25471  xrlimcnp  26118  perfectlem2  26378  rplogsum  26675  perpcom  27074  vtxdgoddnumeven  27920  ex-dif  28787  ococi  29767  orthin  29808  lediri  29899  pjoml2i  29947  pjoml4i  29949  cmcmlem  29953  cmbr3i  29962  cmm2i  29969  cm0  29971  fh1  29980  fh2  29981  cm2j  29982  qlaxr3i  29998  pjclem2  30558  stm1ri  30606  golem1  30633  dmdbr5  30670  mddmd2  30671  cvmdi  30686  mdsldmd1i  30693  csmdsymi  30696  mdexchi  30697  cvexchi  30731  atssma  30740  atomli  30744  atoml2i  30745  atordi  30746  atcvatlem  30747  chirredlem1  30752  chirredlem2  30753  chirredlem3  30754  atcvat4i  30759  atabsi  30763  mdsymlem1  30765  dmdbr6ati  30785  cdj3lem3  30800  inin  30862  difuncomp  30893  iundisj2f  30929  disjunsn  30933  imadifxp  30940  fnresin  30961  fnunres2  31015  mptprop  31031  df1stres  31036  df2ndres  31037  padct  31054  iocinif  31102  difioo  31103  fzodif1  31114  iundisj2fi  31118  xrge00  31295  symgcom  31352  cycpm2tr  31386  cycpmco2f1  31391  xrge0slmod  31548  lindsun  31706  fldexttr  31733  lmxrge0  31902  esumrnmpt2  32036  esumpfinvallem  32042  ldgenpisyslem1  32131  ldgenpisys  32134  measxun2  32178  measunl  32184  carsgclctunlem1  32284  carsgclctunlem2  32286  eulerpartlemt  32338  eulerpartgbij  32339  probmeasb  32397  bayesth  32406  ballotlemfp1  32458  ballotlemfval0  32462  signstres  32554  hashreprin  32600  reprfz1  32604  chtvalz  32609  breprexpnat  32614  f1resrcmplf1d  33059  f1resfz0f1d  33072  subfacp1lem3  33144  subfacp1lem5  33146  pconnconn  33193  cvmscld  33235  cvmsss2  33236  satef  33378  satefvfmla0  33380  mrsubvrs  33484  nosupbnd2lem1  33918  sltlpss  34087  cldbnd  34515  bj-inrab3  35117  bj-2upln1upl  35214  bj-sscon  35219  bj-rest0  35264  bj-0int  35272  bj-ismooredr2  35281  icoreclin  35528  fin2so  35764  ptrest  35776  poimirlem3  35780  poimirlem11  35788  poimirlem12  35789  poimirlem13  35790  poimirlem14  35791  poimirlem15  35792  poimirlem18  35795  poimirlem21  35798  poimirlem22  35799  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  cnambfre  35825  asindmre  35860  dvasin  35861  dvreasin  35863  dvreacos  35864  sstotbnd2  35932  bndss  35944  inres2  36384  redundss3  36741  l1cvat  37069  pmod2iN  37863  pmodN  37864  pmodl42N  37865  osumcllem3N  37972  osumcllem4N  37973  dihmeetlem19N  39339  dihmeetALTN  39341  metakunt18  40142  elrfi  40516  diophrw  40581  eldioph2lem1  40582  eldioph2lem2  40583  diophin  40594  diophren  40635  dnwech  40873  fnwe2lem2  40876  kelac2lem  40889  kelac2  40890  lmhmlnmsplit  40912  pwssplit4  40914  pwfi2f1o  40921  proot1hash  41025  rp-fakeuninass  41123  elcnvcnvintab  41190  relintab  41191  elcnvcnvlem  41207  conrel1d  41271  dfrcl2  41282  iunrelexp0  41310  ntrk0kbimka  41649  hashnzfz  41938  zfregs2VD  42461  iunconnlem2  42555  ssinss2d  42608  restuni4  42670  restuni6  42671  iccdifioo  43053  uzinico2  43100  sumnnodd  43171  limsupvaluz  43249  cncfuni  43427  fouriersw  43772  saliincl  43866  iundjiunlem  43997  iundjiun  43998  caragenuncllem  44050  caragendifcl  44052  hoidmvlelem2  44134  smflimlem1  44306  perfectALTVlem2  45174  rnghmsscmap2  45531  rnghmsubcsetclem1  45533  rnghmsubcsetc  45535  rngccat  45536  rngcid  45537  rngchomrnghmresALTV  45554  rngcifuestrc  45555  funcrngcsetc  45556  rhmsscmap2  45577  rhmsubcsetclem1  45579  rhmsubcsetc  45581  ringccat  45582  ringcid  45583  rhmsscrnghm  45584  rhmsubcrngclem1  45585  rhmsubcrngc  45587  rngcresringcat  45588  funcringcsetc  45593  rngcrescrhm  45643  rhmsubclem3  45646  rhmsubc  45648  rngcrescrhmALTV  45661  rhmsubcALTVlem3  45664  rhmsubcALTVlem4  45665  opndisj  46196  restclssep  46209  seposep  46219  iscnrm3rlem3  46236  iscnrm3rlem8  46241