MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  incom Structured version   Visualization version   GIF version

Theorem incom 4182
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.
StepHypRef Expression
1 rabswap 3494 . 2 {𝑥𝐴𝑥𝐵} = {𝑥𝐵𝑥𝐴}
2 dfin5 3948 . 2 (𝐴𝐵) = {𝑥𝐴𝑥𝐵}
3 dfin5 3948 . 2 (𝐵𝐴) = {𝑥𝐵𝑥𝐴}
41, 2, 33eqtr4i 2859 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2107  {crab 3147  cin 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1533  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-rab 3152  df-in 3947
This theorem is referenced by:  ineq2  4187  sseqin2  4196  in12  4201  in32  4202  in13  4203  in31  4204  inss2  4210  sslin  4215  inss  4219  dfss7  4221  indif1  4252  indifcom  4253  indir  4256  dfsymdif3  4273  dfrab2  4283  0in  4351  disjr  4403  ssdifin0  4434  difdifdir  4440  uneqdifeq  4441  disjtp2  4651  iinrab2  4989  iunin1  4991  iinin1  4998  riinn0  5002  disjprgw  5058  disjprg  5059  disjxun  5061  inex2  5219  inex2g  5221  rescom  5878  resindm  5899  resdmdfsn  5900  resopab  5901  imadisj  5946  intirr  5976  djudisj  6022  imainrect  6036  dmresv  6055  resdmres  6087  coeq0  6106  dfpred3  6156  wfi  6179  ordtri3or  6221  fnresdisj  6464  fnimaeq0  6478  resasplit  6545  fresaun  6546  fresaunres2  6547  fresaunres1  6548  f0rn0  6561  fvun2  6752  fveqressseq  6843  ressnop0  6911  fninfp  6932  fvsnun1  6940  fsnunfv  6945  fveqf1o  7052  orduniss2  7536  offres  7675  curry1  7790  curry2  7793  fpar  7802  wfrlem5  7950  smores3  7981  oacomf1o  8181  ralxpmap  8449  difsnen  8588  domunsncan  8606  domunsn  8656  limensuci  8682  phplem2  8686  pssnn  8725  dif1en  8740  domunfican  8780  marypha1lem  8886  zfregfr  9057  epfrs  9162  zfregs2  9164  djuin  9336  tskwe  9368  dif1card  9425  dfac8b  9446  ac10ct  9449  kmlem11  9575  kmlem12  9576  djucomen  9592  onadju  9608  ackbij1lem14  9644  ackbij1lem16  9646  ackbij1lem18  9648  fin23lem26  9736  fin23lem19  9747  fin23lem30  9753  isf32lem4  9767  isf34lem7  9790  isf34lem6  9791  axdc3lem4  9864  brdom7disj  9942  brdom6disj  9943  fpwwe2lem13  10053  canthp1lem1  10063  grothprim  10245  fzpreddisj  12946  fzdifsuc  12957  fseq1p1m1  12971  prinfzo0  13066  hashgval  13683  hashun3  13735  hashfun  13788  hashbclem  13800  xpcoidgend  14325  cotr2  14327  limsupgle  14824  prmreclem2  16243  setsdm  16507  setsfun  16508  setsfun0  16509  setsid  16528  ressinbas  16550  wunress  16554  mreexexlem2d  16906  mreexexlem4d  16908  oppcinv  17040  cnvps  17812  pmtrmvd  18504  lsmmod2  18722  lsmdisj3  18729  lsmdisjr  18730  lsmdisj2r  18731  lsmdisj3r  18732  lsmdisj2a  18733  lsmdisj2b  18734  lsmdisj3a  18735  lsmdisj3b  18736  subgdisj2  18738  pj2f  18744  pj1id  18745  frgpuplem  18818  gsummptfzsplitl  18973  dprd2da  19084  dmdprdsplit2lem  19087  dmdprdsplit2  19088  pgpfaclem1  19123  lmhmlsp  19741  pwssplit1  19751  ltbwe  20171  psrbag0  20192  cnfldfun  20473  psgndiflemB  20660  pjpm  20768  islindf4  20898  elcls  21597  mretopd  21616  restin  21690  restcld  21696  neitr  21704  resstopn  21710  lecldbas  21743  nrmsep  21881  regsep2  21900  isreg2  21901  ordthaus  21908  cmpsublem  21923  cmpsub  21924  hauscmplem  21930  bwth  21934  iunconn  21952  cldllycmp  22019  kgentopon  22062  llycmpkgen2  22074  1stckgen  22078  txkgen  22176  kqcldsat  22257  regr1lem2  22264  fbun  22364  fin1aufil  22456  fclsfnflim  22551  ustexsym  22739  restutopopn  22762  ustuqtop5  22769  ressuss  22787  metreslem  22887  blcld  23030  ressxms  23050  ressms  23051  restmetu  23095  reconn  23351  metdseq0  23377  metnrmlem3  23384  unmbl  24053  volun  24061  volinun  24062  iundisj2  24065  icombl  24080  ioombl  24081  uniioombllem2  24099  uniioombllem4  24102  dyaddisjlem  24111  dyaddisj  24112  mbfconstlem  24143  mbfeqalem2  24158  ismbf3d  24170  itg1addlem5  24216  itgsplitioo  24353  lhop  24528  tdeglem4  24569  vieta1lem2  24815  xrlimcnp  25460  perfectlem2  25720  rplogsum  26017  perpcom  26413  vtxdgoddnumeven  27249  ex-dif  28116  ococi  29096  orthin  29137  lediri  29228  pjoml2i  29276  pjoml4i  29278  cmcmlem  29282  cmbr3i  29291  cmm2i  29298  cm0  29300  fh1  29309  fh2  29310  cm2j  29311  qlaxr3i  29327  pjclem2  29887  stm1ri  29935  golem1  29962  dmdbr5  29999  mddmd2  30000  cvmdi  30015  mdsldmd1i  30022  csmdsymi  30025  mdexchi  30026  cvexchi  30060  atssma  30069  atomli  30073  atoml2i  30074  atordi  30075  atcvatlem  30076  chirredlem1  30081  chirredlem2  30082  chirredlem3  30083  atcvat4i  30088  atabsi  30092  mdsymlem1  30094  dmdbr6ati  30114  cdj3lem3  30129  disjdifr  30189  inin  30191  difeq  30194  difuncomp  30219  disjdifprg  30240  iundisj2f  30255  disjunsn  30259  imadifxp  30266  fnresin  30286  fnunres2  30339  mptprop  30347  df1stres  30352  df2ndres  30353  padct  30368  iocinif  30417  difioo  30418  fzodif1  30429  iundisj2fi  30433  xrge00  30587  symgcom  30641  tocycfvres1  30666  tocycfvres2  30667  cycpmfvlem  30668  cycpmfv3  30671  cycpmcl  30672  cycpm2tr  30675  cycpmco2f1  30680  xrge0slmod  30831  lindsun  30907  fldexttr  30934  lmxrge0  31081  esumrnmpt2  31213  esumpfinvallem  31219  ldgenpisyslem1  31308  ldgenpisys  31311  measxun2  31355  measunl  31361  carsgclctunlem1  31461  carsgclctunlem2  31463  eulerpartlemt  31515  eulerpartgbij  31516  probmeasb  31574  bayesth  31583  ballotlemfp1  31635  ballotlemfval0  31639  signstres  31731  hashreprin  31777  reprfz1  31781  chtvalz  31786  breprexpnat  31791  f1resrcmplf1d  32244  f1resfz0f1d  32245  subfacp1lem3  32313  subfacp1lem5  32315  pconnconn  32362  cvmscld  32404  cvmsss2  32405  satef  32547  satefvfmla0  32549  mrsubvrs  32653  mthmpps  32713  frpoind  32964  frind  32969  fprlem1  33021  frrlem15  33026  nosupbnd2lem1  33099  noetalem2  33102  noetalem3  33103  cldbnd  33558  bj-inrab3  34131  bj-2upln1upl  34220  bj-sscon  34225  bj-rest0  34265  bj-0int  34274  bj-ismooredr2  34283  icoreclin  34507  fin2so  34746  ptrest  34758  poimirlem3  34762  poimirlem11  34770  poimirlem12  34771  poimirlem13  34772  poimirlem14  34773  poimirlem15  34774  poimirlem16  34775  poimirlem18  34777  poimirlem19  34778  poimirlem21  34780  poimirlem22  34781  poimirlem27  34786  mblfinlem3  34798  mblfinlem4  34799  ismblfin  34800  cnambfre  34807  asindmre  34844  dvasin  34845  dvreasin  34847  dvreacos  34848  sstotbnd2  34920  bndss  34932  ineqcom  35372  inres2  35374  redundss3  35730  l1cvat  36058  pmod2iN  36852  pmodN  36853  pmodl42N  36854  osumcllem3N  36961  osumcllem4N  36962  dihmeetlem19N  38328  dihmeetALTN  38330  elrfi  39156  diophrw  39221  eldioph2lem1  39222  eldioph2lem2  39223  diophin  39234  diophren  39275  dnwech  39513  fnwe2lem2  39516  kelac1  39528  kelac2lem  39529  kelac2  39530  lmhmlnmsplit  39552  pwssplit4  39554  pwfi2f1o  39561  proot1hash  39665  rp-fakeuninass  39747  elcnvcnvintab  39807  relintab  39808  elcnvcnvlem  39824  conrel1d  39873  dfrcl2  39884  iunrelexp0  39912  ntrk0kbimka  40254  hashnzfz  40517  zfregs2VD  41040  iunconnlem2  41134  ssinss2d  41187  restuni4  41253  restuni6  41254  iccdifioo  41656  uzinico2  41703  sumnnodd  41776  limsupvaluz  41854  cncfuni  42034  fouriersw  42382  saliincl  42476  iundjiunlem  42607  iundjiun  42608  caragenuncllem  42660  caragendifcl  42662  isomenndlem  42678  hoidmvlelem2  42744  smflimlem1  42913  perfectALTVlem2  43719  rnghmsscmap2  44076  rnghmsubcsetclem1  44078  rnghmsubcsetc  44080  rngccat  44081  rngcid  44082  rngchomrnghmresALTV  44099  rngcifuestrc  44100  funcrngcsetc  44101  rhmsscmap2  44122  rhmsubcsetclem1  44124  rhmsubcsetc  44126  ringccat  44127  ringcid  44128  rhmsscrnghm  44129  rhmsubcrngclem1  44130  rhmsubcrngc  44132  rngcresringcat  44133  funcringcsetc  44138  rngcrescrhm  44188  rhmsubclem3  44191  rhmsubc  44193  rngcrescrhmALTV  44206  rhmsubcALTVlem3  44209  rhmsubcALTVlem4  44210
  Copyright terms: Public domain W3C validator