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

Theorem incom 3998
Description: Commutative law for intersection of classes. Exercise 7 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
incom (𝐴𝐵) = (𝐵𝐴)

Proof of Theorem incom
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ancom 450 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elin 3989 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3989 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
41, 2, 33bitr4i 294 . 2 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
54eqriv 2799 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wcel 2155  cin 3762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-in 3770
This theorem is referenced by:  ineq2  4001  sseqin2  4010  in12  4015  in32  4016  in13  4017  in31  4018  inss2  4024  sslin  4029  inss  4033  indif1  4067  indifcom  4068  indir  4071  dfsymdif3  4088  dfrab2  4098  0in  4161  disjr  4209  ssdifin0  4240  difdifdir  4246  uneqdifeq  4247  disjtp2  4437  iinrab2  4768  iunin1  4770  iinin1  4776  riinn0  4780  disjprg  4833  disjxun  4835  inex2  4989  dmres  5616  rescom  5620  resindm  5643  resdmdfsn  5644  resopab  5645  imadisj  5688  intirr  5719  djudisj  5766  imainrect  5780  dmresv  5798  resdmres  5833  coeq0  5852  dfpred3  5897  wfi  5920  ordtri3or  5962  fnresdisj  6206  fnimaeq0  6218  resasplit  6283  fresaun  6284  fresaunres2  6285  fresaunres1  6286  f0rn0  6299  fvun2  6485  fveqressseq  6571  ressnop0  6638  fninfp  6659  fvsnun1  6667  fsnunfv  6672  fveqf1o  6775  orduniss2  7257  offres  7387  curry1  7497  curry2  7500  fpar  7509  wfrlem5  7649  smores3  7680  oacomf1o  7876  ralxpmap  8138  difsnen  8275  domunsncan  8293  domunsn  8343  limensuci  8369  phplem2  8373  pssnn  8411  dif1en  8426  domunfican  8466  marypha1lem  8572  zfregfr  8742  epfrs  8848  zfregs2  8850  djuin  9021  tskwe  9053  dif1card  9110  dfac8b  9131  ac10ct  9134  kmlem11  9261  kmlem12  9262  cdacomen  9282  onacda  9298  ackbij1lem14  9334  ackbij1lem16  9336  ackbij1lem18  9338  fin23lem26  9426  fin23lem19  9437  fin23lem30  9443  isf32lem4  9457  isf34lem7  9480  isf34lem6  9481  axdc3lem4  9554  brdom7disj  9632  brdom6disj  9633  fpwwe2lem13  9743  canthp1lem1  9753  grothprim  9935  fzpreddisj  12607  fzdifsuc  12617  fseq1p1m1  12631  prinfzo0  12725  hashgval  13334  hashun3  13385  hashfun  13435  hashbclem  13447  xpcoidgend  13933  cotr2  13935  limsupgle  14425  prmreclem2  15832  setsdm  16097  setsfun  16098  setsfun0  16099  setsid  16119  ressinbas  16141  wunress  16146  mreexexlem2d  16504  mreexexlem4d  16506  oppcinv  16638  cnvps  17411  pmtrmvd  18071  lsmmod2  18284  lsmdisj3  18291  lsmdisjr  18292  lsmdisj2r  18293  lsmdisj3r  18294  lsmdisj2a  18295  lsmdisj2b  18296  lsmdisj3a  18297  lsmdisj3b  18298  subgdisj2  18300  pj2f  18306  pj1id  18307  frgpuplem  18380  gsummptfzsplitl  18528  dprd2da  18637  dmdprdsplit2lem  18640  dmdprdsplit2  18641  pgpfaclem1  18676  lmhmlsp  19250  pwssplit1  19260  ltbwe  19675  psrbag0  19696  cnfldfun  19960  psgndiflemB  20148  pjpm  20256  islindf4  20381  elcls  21085  mretopd  21104  restin  21178  restcld  21184  neitr  21192  resstopn  21198  lecldbas  21231  nrmsep  21369  regsep2  21388  isreg2  21389  ordthaus  21396  cmpsublem  21410  cmpsub  21411  hauscmplem  21417  bwth  21421  iunconn  21439  cldllycmp  21506  kgentopon  21549  llycmpkgen2  21561  1stckgen  21565  txkgen  21663  kqcldsat  21744  regr1lem2  21751  fbun  21851  fin1aufil  21943  fclsfnflim  22038  ustexsym  22226  restutopopn  22249  ustuqtop5  22256  ressuss  22274  metreslem  22374  blcld  22517  ressxms  22537  ressms  22538  restmetu  22582  reconn  22838  metdseq0  22864  metnrmlem3  22871  unmbl  23512  volun  23520  volinun  23521  iundisj2  23524  icombl  23539  ioombl  23540  uniioombllem2  23558  uniioombllem4  23561  dyaddisjlem  23570  dyaddisj  23571  mbfconstlem  23602  mbfeqalem2  23617  ismbf3d  23629  itg1addlem5  23675  itgsplitioo  23812  lhop  23987  tdeglem4  24028  vieta1lem2  24274  xrlimcnp  24903  perfectlem2  25163  rplogsum  25424  perpcom  25816  vtxdgoddnumeven  26671  ex-dif  27605  ococi  28586  orthin  28627  lediri  28718  pjoml2i  28766  pjoml4i  28768  cmcmlem  28772  cmbr3i  28781  cmm2i  28788  cm0  28790  fh1  28799  fh2  28800  cm2j  28801  qlaxr3i  28817  pjclem2  29377  stm1ri  29425  golem1  29452  dmdbr5  29489  mddmd2  29490  cvmdi  29505  mdsldmd1i  29512  csmdsymi  29515  mdexchi  29516  cvexchi  29550  atssma  29559  atomli  29563  atoml2i  29564  atordi  29565  atcvatlem  29566  chirredlem1  29571  chirredlem2  29572  chirredlem3  29573  atcvat4i  29578  atabsi  29582  mdsymlem1  29584  dmdbr6ati  29604  cdj3lem3  29619  inin  29671  difeq  29674  difuncomp  29688  disjdifprg  29707  iundisj2f  29722  disjunsn  29726  imadifxp  29733  fnresin  29751  df1stres  29802  df2ndres  29803  padct  29818  iocinif  29864  difioo  29865  iundisj2fi  29877  xrge00  30005  xrge0slmod  30163  lmxrge0  30317  esumrnmpt2  30449  esumpfinvallem  30455  ldgenpisyslem1  30545  ldgenpisys  30548  measxun2  30592  measunl  30598  carsgclctunlem1  30698  carsgclctunlem2  30700  eulerpartlemt  30752  eulerpartgbij  30753  probmeasb  30811  bayesth  30820  ballotlemfp1  30872  ballotlemfval0  30876  signstres  30971  hashreprin  31017  reprfz1  31021  chtvalz  31026  breprexpnat  31031  subfacp1lem3  31481  subfacp1lem5  31483  pconnconn  31530  cvmscld  31572  cvmsss2  31573  mrsubvrs  31736  mthmpps  31796  frpoind  32055  frind  32058  frrlem5  32099  nosupbnd2lem1  32176  noetalem2  32179  noetalem3  32180  cldbnd  32636  bj-inrab3  33230  bj-2upln1upl  33316  bj-sscon  33318  bj-rest0  33351  bj-0int  33360  bj-diagval  33401  icoreclin  33515  fin2so  33703  ptrest  33715  poimirlem3  33719  poimirlem11  33727  poimirlem12  33728  poimirlem13  33729  poimirlem14  33730  poimirlem15  33731  poimirlem16  33732  poimirlem18  33734  poimirlem19  33735  poimirlem21  33737  poimirlem22  33738  poimirlem27  33743  mblfinlem3  33755  mblfinlem4  33756  ismblfin  33757  cnambfre  33764  asindmre  33801  dvasin  33802  dvreasin  33804  dvreacos  33805  sstotbnd2  33878  bndss  33890  ineqcom  34320  inres2  34322  inex2ALTV  34414  l1cvat  34829  pmod2iN  35623  pmodN  35624  pmodl42N  35625  osumcllem3N  35732  osumcllem4N  35733  dihmeetlem19N  37100  dihmeetALTN  37102  elrfi  37753  diophrw  37818  eldioph2lem1  37819  eldioph2lem2  37820  diophin  37832  diophren  37873  dnwech  38113  fnwe2lem2  38116  kelac1  38128  kelac2lem  38129  kelac2  38130  lmhmlnmsplit  38152  pwssplit4  38154  pwfi2f1o  38161  proot1hash  38273  rp-fakeuninass  38356  elcnvcnvintab  38382  relintab  38383  elcnvcnvlem  38399  conrel1d  38449  dfrcl2  38460  iunrelexp0  38488  ntrk0kbimka  38831  neicvgbex  38904  hashnzfz  39013  zfregs2VD  39564  iunconnlem2  39659  ssinss2d  39715  restuni4  39790  restuni6  39791  iccdifioo  40216  uzinico2  40263  sumnnodd  40336  limsupvaluz  40414  cncfuni  40573  fouriersw  40921  saliincl  41018  iundjiunlem  41149  iundjiun  41150  caragenuncllem  41202  caragendifcl  41204  isomenndlem  41220  hoidmvlelem2  41286  smflimlem1  41455  dfss7  41861  perfectALTVlem2  42200  rnghmsscmap2  42535  rnghmsubcsetclem1  42537  rnghmsubcsetc  42539  rngccat  42540  rngcid  42541  rngchomrnghmresALTV  42558  rngcifuestrc  42559  funcrngcsetc  42560  rhmsscmap2  42581  rhmsubcsetclem1  42583  rhmsubcsetc  42585  ringccat  42586  ringcid  42587  rhmsscrnghm  42588  rhmsubcrngclem1  42589  rhmsubcrngc  42591  rngcresringcat  42592  funcringcsetc  42597  rngcrescrhm  42647  rhmsubclem3  42650  rhmsubc  42652  rngcrescrhmALTV  42665  rhmsubcALTVlem3  42668  rhmsubcALTVlem4  42669
  Copyright terms: Public domain W3C validator