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

Theorem incom 3838
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 465 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elin 3829 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3829 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
41, 2, 33bitr4i 292 . 2 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
54eqriv 2648 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1523  wcel 2030  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614
This theorem is referenced by:  ineq2  3841  sseqin2  3850  dfss1OLD  3851  in12  3857  in32  3858  in13  3859  in31  3860  inss2  3867  sslin  3872  inss  3875  indif1  3904  indifcom  3905  indir  3908  dfsymdif3  3926  dfrab2  3936  0in  4002  disjr  4051  ssdifin0  4083  difdifdir  4089  uneqdifeq  4090  uneqdifeqOLD  4091  disjtp2  4284  diftpsn3OLD  4365  iinrab2  4615  iunin1  4617  iinin1  4623  riinn0  4627  disjprg  4680  disjxun  4683  inex2  4833  resiun1OLD  5452  dmres  5454  rescom  5458  resima2OLD  5468  resindm  5479  resdmdfsn  5480  resopab  5481  imadisj  5519  intirr  5549  djudisj  5596  imainrect  5610  dmresv  5628  resdmres  5663  coeq0  5682  dfpred3  5728  wfi  5751  ordtri3or  5793  fnresdisj  6039  fnimaeq0  6051  resasplit  6112  fresaun  6113  fresaunres2  6114  fresaunres1  6115  f0rn0  6128  fvun2  6309  fveqressseq  6395  ressnop0  6460  fninfp  6481  fvsnun1  6489  fsnunfv  6494  fveqf1o  6597  orduniss2  7075  offres  7205  curry1  7314  curry2  7317  fpar  7326  wfrlem5  7464  smores3  7495  oacomf1o  7690  ralxpmap  7949  difsnen  8083  domunsncan  8101  domunsn  8151  limensuci  8177  phplem2  8181  pssnn  8219  dif1en  8234  domunfican  8274  marypha1lem  8380  zfregfr  8547  epfrs  8645  zfregs2  8647  tskwe  8814  dif1card  8871  dfac8b  8892  ac10ct  8895  kmlem11  9020  kmlem12  9021  cdacomen  9041  onacda  9057  ackbij1lem14  9093  ackbij1lem16  9095  ackbij1lem18  9097  fin23lem26  9185  fin23lem19  9196  fin23lem30  9202  isf32lem4  9216  isf34lem7  9239  isf34lem6  9240  axdc3lem4  9313  brdom7disj  9391  brdom6disj  9392  fpwwe2lem13  9502  canthp1lem1  9512  grothprim  9694  fzpreddisj  12428  fzdifsuc  12438  fseq1p1m1  12452  prinfzo0  12546  hashgval  13160  hashun3  13211  hashfun  13262  hashbclem  13274  xpcoidgend  13760  cotr2  13762  limsupgle  14252  prmreclem2  15668  setsdm  15939  setsfun  15940  setsfun0  15941  setsid  15961  ressinbas  15983  wunress  15987  mreexexlem2d  16352  mreexexlem4d  16354  oppcinv  16487  cnvps  17259  pmtrmvd  17922  lsmmod2  18135  lsmdisj3  18142  lsmdisjr  18143  lsmdisj2r  18144  lsmdisj3r  18145  lsmdisj2a  18146  lsmdisj2b  18147  lsmdisj3a  18148  lsmdisj3b  18149  subgdisj2  18151  pj2f  18157  pj1id  18158  frgpuplem  18231  gsummptfzsplitl  18379  dprd2da  18487  dmdprdsplit2lem  18490  dmdprdsplit2  18491  pgpfaclem1  18526  lmhmlsp  19097  pwssplit1  19107  ltbwe  19520  psrbag0  19542  cnfldfun  19806  psgndiflemB  19994  pjpm  20100  islindf4  20225  elcls  20925  mretopd  20944  restin  21018  restcld  21024  neitr  21032  resstopn  21038  lecldbas  21071  nrmsep  21209  regsep2  21228  isreg2  21229  ordthaus  21236  cmpsublem  21250  cmpsub  21251  hauscmplem  21257  bwth  21261  iunconn  21279  cldllycmp  21346  kgentopon  21389  llycmpkgen2  21401  1stckgen  21405  txkgen  21503  kqcldsat  21584  regr1lem2  21591  fbun  21691  fin1aufil  21783  fclsfnflim  21878  ustexsym  22066  restutopopn  22089  ustuqtop5  22096  ressuss  22114  metreslem  22214  blcld  22357  ressxms  22377  ressms  22378  restmetu  22422  reconn  22678  metdseq0  22704  metnrmlem3  22711  unmbl  23351  volun  23359  volinun  23360  iundisj2  23363  icombl  23378  ioombl  23379  uniioombllem2  23397  uniioombllem4  23400  dyaddisjlem  23409  dyaddisj  23410  mbfconstlem  23441  mbfeqalem  23454  ismbf3d  23466  itg1addlem5  23512  itgsplitioo  23649  lhop  23824  tdeglem4  23865  vieta1lem2  24111  xrlimcnp  24740  perfectlem2  25000  rplogsum  25261  perpcom  25653  vtxdgoddnumeven  26505  ex-dif  27410  ococi  28392  orthin  28433  lediri  28524  pjoml2i  28572  pjoml4i  28574  cmcmlem  28578  cmbr3i  28587  cmm2i  28594  cm0  28596  fh1  28605  fh2  28606  cm2j  28607  qlaxr3i  28623  pjclem2  29183  stm1ri  29231  golem1  29258  dmdbr5  29295  mddmd2  29296  cvmdi  29311  mdsldmd1i  29318  csmdsymi  29321  mdexchi  29322  cvexchi  29356  atssma  29365  atomli  29369  atoml2i  29370  atordi  29371  atcvatlem  29372  chirredlem1  29377  chirredlem2  29378  chirredlem3  29379  atcvat4i  29384  atabsi  29388  mdsymlem1  29390  dmdbr6ati  29410  cdj3lem3  29425  inin  29478  difeq  29481  difuncomp  29495  disjdifprg  29514  iundisj2f  29529  disjunsn  29533  imadifxp  29540  fnresin  29558  df1stres  29609  df2ndres  29610  padct  29625  iocinif  29671  difioo  29672  iundisj2fi  29684  xrge00  29814  xrge0slmod  29972  lmxrge0  30126  esumrnmpt2  30258  esumpfinvallem  30264  ldgenpisyslem1  30354  ldgenpisys  30357  measxun2  30401  measunl  30407  carsgclctunlem1  30507  carsgclctunlem2  30509  eulerpartlemt  30561  eulerpartgbij  30562  probmeasb  30620  bayesth  30629  ballotlemfp1  30681  ballotlemfval0  30685  signstres  30780  hashreprin  30826  reprfz1  30830  chtvalz  30835  breprexpnat  30840  subfacp1lem3  31290  subfacp1lem5  31292  pconnconn  31339  cvmscld  31381  cvmsss2  31382  mrsubvrs  31545  mthmpps  31605  frpoind  31865  frind  31868  frrlem5  31909  nosupbnd2lem1  31986  noetalem2  31989  noetalem3  31990  cldbnd  32446  bj-inrab3  33050  bj-2upln1upl  33137  bj-sscon  33139  bj-rest0  33171  bj-0int  33180  bj-diagval  33220  icoreclin  33335  fin2so  33526  ptrest  33538  poimirlem3  33542  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem18  33557  poimirlem19  33558  poimirlem21  33560  poimirlem22  33561  poimirlem27  33566  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  cnambfre  33588  asindmre  33625  dvasin  33626  dvreasin  33628  dvreacos  33629  sstotbnd2  33703  bndss  33715  ineqcom  34148  inres2  34150  inex2ALTV  34246  l1cvat  34660  pmod2iN  35453  pmodN  35454  pmodl42N  35455  osumcllem3N  35562  osumcllem4N  35563  dihmeetlem19N  36931  dihmeetALTN  36933  elrfi  37574  diophrw  37639  eldioph2lem1  37640  eldioph2lem2  37641  diophin  37653  diophren  37694  dnwech  37935  fnwe2lem2  37938  kelac1  37950  kelac2lem  37951  kelac2  37952  lmhmlnmsplit  37974  pwssplit4  37976  pwfi2f1o  37983  proot1hash  38095  rp-fakeuninass  38179  elcnvcnvintab  38205  relintab  38206  elcnvcnvlem  38222  conrel1d  38272  dfrcl2  38283  iunrelexp0  38311  ntrk0kbimka  38654  neicvgbex  38727  hashnzfz  38836  zfregs2VD  39390  iunconnlem2  39485  ssinss2d  39542  restuni4  39618  restuni6  39619  iccdifioo  40059  uzinico2  40107  sumnnodd  40180  limsupvaluz  40258  cncfuni  40417  fouriersw  40766  saliincl  40863  iundjiunlem  40994  iundjiun  40995  caragenuncllem  41047  caragendifcl  41049  isomenndlem  41065  hoidmvlelem2  41131  smflimlem1  41300  perfectALTVlem2  41956  rnghmsscmap2  42298  rnghmsubcsetclem1  42300  rnghmsubcsetc  42302  rngccat  42303  rngcid  42304  rngchomrnghmresALTV  42321  rngcifuestrc  42322  funcrngcsetc  42323  rhmsscmap2  42344  rhmsubcsetclem1  42346  rhmsubcsetc  42348  ringccat  42349  ringcid  42350  rhmsscrnghm  42351  rhmsubcrngclem1  42352  rhmsubcrngc  42354  rngcresringcat  42355  funcringcsetc  42360  rngcrescrhm  42410  rhmsubclem3  42413  rhmsubc  42415  rngcrescrhmALTV  42428  rhmsubcALTVlem3  42431  rhmsubcALTVlem4  42432
  Copyright terms: Public domain W3C validator