Theorem incom 4200

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  {crab 3433   ∩ cin 3946

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434  df-in 3954

This theorem is referenced by:  ineqcom  4201  ineqcomi  4202  ineq2  4205  sseqin2  4214  in12  4219  in32  4220  in13  4221  in31  4222  inss2  4228  sslin  4233  inss  4237  dfss7  4239  indif1  4270  indifcom  4271  indir  4274  indifdir  4283  dfsymdif3  4295  dfrab2  4309  0in  4392  disjr  4448  disjdifr  4471  difdifdir  4490  uneqdifeq  4491  disjtp2  4719  iinrab2  5072  iunin1  5074  iinin1  5081  riinn0  5085  disjprgw  5142  disjprg  5143  disjxun  5145  inex2  5317  inex2g  5319  rescom  6005  resindm  6028  resdmdfsn  6029  resopab  6032  imadisj  6076  intirr  6116  djudisj  6163  imainrect  6177  dmresv  6196  resdmres  6228  coeq0  6251  dfpred3  6308  predres  6337  frpoind  6340  wfiOLD  6349  ordtri3or  6393  fnresdisj  6667  fnimaeq0  6680  resasplit  6758  fresaun  6759  fresaunres2  6760  fresaunres1  6761  f0rn0  6773  fvun2  6979  rescnvimafod  7071  fveqressseq  7077  ressnop0  7146  fninfp  7167  fsnunfv  7180  orduniss2  7816  offres  7965  curry1  8085  curry2  8088  fpar  8097  fprlem1  8280  wfrlem5OLD  8308  smores3  8348  oacomf1o  8561  domunsncan  9068  phplem2OLD  9214  pssnnOLD  9261  dif1ennnALT  9273  domunfican  9316  marypha1lem  9424  zfregfr  9596  epfrs  9722  zfregs2  9724  frind  9741  frrlem15  9748  djuin  9909  tskwe  9941  dfac8b  10022  ac10ct  10025  kmlem11  10151  kmlem12  10152  djucomen  10168  onadju  10184  ackbij1lem14  10224  ackbij1lem16  10226  fin23lem26  10316  fin23lem19  10327  fin23lem30  10333  isf32lem4  10347  isf34lem7  10370  isf34lem6  10371  axdc3lem4  10444  brdom7disj  10522  brdom6disj  10523  fpwwe2lem12  10633  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  18527  pmtrmvd  19317  lsmmod2  19537  lsmdisj3  19544  lsmdisjr  19545  lsmdisj2r  19546  lsmdisj3r  19547  lsmdisj2a  19548  lsmdisj2b  19549  lsmdisj3a  19550  lsmdisj3b  19551  subgdisj2  19553  pj2f  19559  pj1id  19560  frgpuplem  19633  gsummptfzsplitl  19793  dprd2da  19904  dmdprdsplit2lem  19907  dmdprdsplit2  19908  pgpfaclem1  19943  lmhmlsp  20648  cnfldfunALTOLD  20943  psgndiflemB  21137  pjpm  21247  ltbwe  21581  psrbag0  21605  elcls  22559  mretopd  22578  restin  22652  restcld  22658  resstopn  22672  lecldbas  22705  nrmsep  22843  isreg2  22863  ordthaus  22870  cmpsublem  22885  cmpsub  22886  hauscmplem  22892  bwth  22896  iunconn  22914  cldllycmp  22981  kgentopon  23024  llycmpkgen2  23036  1stckgen  23040  txkgen  23138  kqcldsat  23219  regr1lem2  23226  fbun  23326  fin1aufil  23418  fclsfnflim  23513  ustexsym  23702  restutopopn  23725  ustuqtop5  23732  ressuss  23749  metreslem  23850  blcld  23996  ressxms  24016  ressms  24017  reconn  24326  metdseq0  24352  metnrmlem3  24359  unmbl  25036  volun  25044  iundisj2  25048  icombl  25063  ioombl  25064  uniioombllem2  25082  uniioombllem4  25085  dyaddisjlem  25094  dyaddisj  25095  mbfconstlem  25126  mbfeqalem2  25141  ismbf3d  25153  itg1addlem5  25200  itgsplitioo  25337  lhop  25515  tdeglem4OLD  25560  vieta1lem2  25806  xrlimcnp  26453  perfectlem2  26713  rplogsum  27010  nosupbnd2lem1  27198  sltlpss  27381  perpcom  27944  vtxdgoddnumeven  28790  ex-dif  29656  ococi  30636  orthin  30677  lediri  30768  pjoml2i  30816  pjoml4i  30818  cmcmlem  30822  cmbr3i  30831  cmm2i  30838  cm0  30840  fh1  30849  fh2  30850  cm2j  30851  qlaxr3i  30867  pjclem2  31427  stm1ri  31475  golem1  31502  dmdbr5  31539  mddmd2  31540  cvmdi  31555  mdsldmd1i  31562  csmdsymi  31565  mdexchi  31566  cvexchi  31600  atssma  31609  atomli  31613  atoml2i  31614  atordi  31615  atcvatlem  31616  chirredlem1  31621  chirredlem2  31622  chirredlem3  31623  atcvat4i  31628  atabsi  31632  mdsymlem1  31634  dmdbr6ati  31654  cdj3lem3  31669  inin  31731  difuncomp  31763  iundisj2f  31799  disjunsn  31803  imadifxp  31810  fnresin  31828  mptiffisupp  31893  mptprop  31898  df1stres  31903  df2ndres  31904  padct  31922  iocinif  31970  difioo  31971  fzodif1  31982  iundisj2fi  31986  xrge00  32165  symgcom  32222  cycpm2tr  32256  cycpmco2f1  32261  xrge0slmod  32432  oppr2idl  32553  lindsun  32655  fldexttr  32682  lmxrge0  32870  esumrnmpt2  33004  esumpfinvallem  33010  ldgenpisyslem1  33099  ldgenpisys  33102  measxun2  33146  measunl  33152  carsgclctunlem1  33254  carsgclctunlem2  33256  eulerpartlemt  33308  eulerpartgbij  33309  probmeasb  33367  bayesth  33376  ballotlemfp1  33428  ballotlemfval0  33432  signstres  33524  hashreprin  33570  reprfz1  33574  chtvalz  33579  breprexpnat  33584  f1resrcmplf1d  34028  f1resfz0f1d  34041  subfacp1lem3  34111  subfacp1lem5  34113  pconnconn  34160  cvmscld  34202  cvmsss2  34203  satef  34345  satefvfmla0  34347  mrsubvrs  34451  cldbnd  35149  bj-inrab3  35747  bj-2upln1upl  35843  bj-sscon  35848  bj-rest0  35912  bj-0int  35920  bj-ismooredr2  35929  icoreclin  36176  fin2so  36413  ptrest  36425  poimirlem3  36429  poimirlem11  36437  poimirlem12  36438  poimirlem13  36439  poimirlem14  36440  poimirlem15  36441  poimirlem18  36444  poimirlem21  36447  poimirlem22  36448  mblfinlem3  36465  mblfinlem4  36466  ismblfin  36467  cnambfre  36474  asindmre  36509  dvasin  36510  dvreasin  36512  dvreacos  36513  sstotbnd2  36580  bndss  36592  inres2  37050  disjressuc2  37196  redundss3  37436  l1cvat  37863  pmod2iN  38658  pmodN  38659  pmodl42N  38660  osumcllem3N  38767  osumcllem4N  38768  dihmeetlem19N  40134  dihmeetALTN  40136  metakunt18  40940  elrfi  41365  diophrw  41430  eldioph2lem1  41431  eldioph2lem2  41432  diophin  41443  diophren  41484  dnwech  41723  fnwe2lem2  41726  kelac2lem  41739  kelac2  41740  lmhmlnmsplit  41762  pwssplit4  41764  pwfi2f1o  41771  proot1hash  41875  naddov4  42066  rp-fakeuninass  42200  elcnvcnvintab  42266  relintab  42267  elcnvcnvlem  42283  conrel1d  42347  dfrcl2  42358  iunrelexp0  42386  ntrk0kbimka  42723  hashnzfz  43012  zfregs2VD  43535  iunconnlem2  43629  ssinss2d  43680  restuni4  43743  restuni6  43744  restsubel  43780  iccdifioo  44163  uzinico2  44210  sumnnodd  44281  limsupvaluz  44359  cncfuni  44537  fouriersw  44882  saliinclf  44977  iundjiunlem  45110  iundjiun  45111  caragenuncllem  45163  caragendifcl  45165  hoidmvlelem2  45247  smflimlem1  45422  perfectALTVlem2  46325  rnghmsscmap2  46773  rnghmsubcsetclem1  46775  rnghmsubcsetc  46777  rngccat  46778  rngcid  46779  rngchomrnghmresALTV  46796  rngcifuestrc  46797  funcrngcsetc  46798  rhmsscmap2  46819  rhmsubcsetclem1  46821  rhmsubcsetc  46823  ringccat  46824  ringcid  46825  rhmsscrnghm  46826  rhmsubcrngclem1  46827  rhmsubcrngc  46829  rngcresringcat  46830  funcringcsetc  46835  rngcrescrhm  46885  rhmsubclem3  46888  rhmsubc  46890  rngcrescrhmALTV  46903  rhmsubcALTVlem3  46906  rhmsubcALTVlem4  46907  opndisj  47437  restclssep  47450  seposep  47460  iscnrm3rlem3  47477  iscnrm3rlem8  47482