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

Theorem incom 3789
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 466 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elin 3780 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3780 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
41, 2, 33bitr4i 292 . 2 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
54eqriv 2618 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1480  wcel 1987  cin 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-in 3567
This theorem is referenced by:  ineq2  3792  sseqin2  3801  dfss1OLD  3802  in12  3808  in32  3809  in13  3810  in31  3811  inss2  3818  sslin  3823  inss  3826  indif1  3853  indifcom  3854  indir  3857  dfsymdif3  3875  dfrab2  3885  0in  3947  disjr  3996  ssdifin0  4028  difdifdir  4034  uneqdifeq  4035  uneqdifeqOLD  4036  disjtp2  4229  diftpsn3OLD  4309  iinrab2  4556  iunin1  4558  iinin1  4564  riinn0  4568  disjprg  4618  disjxun  4621  inex2  4770  resiun1OLD  5386  dmres  5388  rescom  5392  resima2OLD  5402  resindm  5413  resdmdfsn  5414  resopab  5415  imadisj  5453  intirr  5483  djudisj  5530  imainrect  5544  dmresv  5562  resdmres  5594  coeq0  5613  dfpred3  5659  wfi  5682  ordtri3or  5724  fnresdisj  5969  fnimaeq0  5980  resasplit  6041  fresaun  6042  fresaunres2  6043  fresaunres1  6044  f0rn0  6057  fvun2  6237  fveqressseq  6321  ressnop0  6385  fninfp  6405  fvsnun1  6413  fsnunfv  6418  fveqf1o  6522  orduniss2  6995  offres  7123  curry1  7229  curry2  7232  fpar  7241  wfrlem5  7379  smores3  7410  oacomf1o  7605  ralxpmap  7867  difsnen  8002  domunsncan  8020  domunsn  8070  limensuci  8096  phplem2  8100  pssnn  8138  dif1en  8153  domunfican  8193  marypha1lem  8299  zfregfr  8469  epfrs  8567  zfregs2  8569  tskwe  8736  dif1card  8793  dfac8b  8814  ac10ct  8817  kmlem11  8942  kmlem12  8943  cdacomen  8963  onacda  8979  ackbij1lem14  9015  ackbij1lem16  9017  ackbij1lem18  9019  fin23lem26  9107  fin23lem19  9118  fin23lem30  9124  isf32lem4  9138  isf34lem7  9161  isf34lem6  9162  axdc3lem4  9235  brdom7disj  9313  brdom6disj  9314  fpwwe2lem13  9424  canthp1lem1  9434  grothprim  9616  fzpreddisj  12348  fzdifsuc  12358  fseq1p1m1  12371  prinfzo0  12463  hashgval  13076  hashun3  13129  hashfun  13180  hashbclem  13190  xpcoidgend  13664  cotr2  13666  limsupgle  14158  prmreclem2  15564  setsdm  15832  setsfun  15833  setsfun0  15834  setsid  15854  ressinbas  15876  wunress  15880  mreexexlem2d  16245  mreexexlem4d  16247  oppcinv  16380  cnvps  17152  pmtrmvd  17816  lsmmod2  18029  lsmdisj3  18036  lsmdisjr  18037  lsmdisj2r  18038  lsmdisj3r  18039  lsmdisj2a  18040  lsmdisj2b  18041  lsmdisj3a  18042  lsmdisj3b  18043  subgdisj2  18045  pj2f  18051  pj1id  18052  frgpuplem  18125  gsummptfzsplitl  18273  dprd2da  18381  dmdprdsplit2lem  18384  dmdprdsplit2  18385  pgpfaclem1  18420  lmhmlsp  18989  pwssplit1  18999  ltbwe  19412  psrbag0  19434  cnfldfun  19698  psgndiflemB  19886  pjpm  19992  islindf4  20117  elcls  20817  mretopd  20836  restin  20910  restcld  20916  neitr  20924  resstopn  20930  lecldbas  20963  nrmsep  21101  regsep2  21120  isreg2  21121  ordthaus  21128  cmpsublem  21142  cmpsub  21143  hauscmplem  21149  bwth  21153  iunconn  21171  cldllycmp  21238  kgentopon  21281  llycmpkgen2  21293  1stckgen  21297  txkgen  21395  kqcldsat  21476  regr1lem2  21483  fbun  21584  fin1aufil  21676  fclsfnflim  21771  ustexsym  21959  restutopopn  21982  ustuqtop5  21989  ressuss  22007  metreslem  22107  blcld  22250  ressxms  22270  ressms  22271  restmetu  22315  reconn  22571  metdseq0  22597  metnrmlem3  22604  unmbl  23245  volun  23253  volinun  23254  iundisj2  23257  icombl  23272  ioombl  23273  uniioombllem2  23291  uniioombllem4  23294  dyaddisjlem  23303  dyaddisj  23304  mbfconstlem  23336  mbfeqalem  23349  ismbf3d  23361  itg1addlem5  23407  itgsplitioo  23544  lhop  23717  tdeglem4  23758  vieta1lem2  24004  xrlimcnp  24629  perfectlem2  24889  rplogsum  25150  perpcom  25542  ex-dif  27168  ococi  28152  orthin  28193  lediri  28284  pjoml2i  28332  pjoml4i  28334  cmcmlem  28338  cmbr3i  28347  cmm2i  28354  cm0  28356  fh1  28365  fh2  28366  cm2j  28367  qlaxr3i  28383  pjclem2  28943  stm1ri  28991  golem1  29018  dmdbr5  29055  mddmd2  29056  cvmdi  29071  mdsldmd1i  29078  csmdsymi  29081  mdexchi  29082  cvexchi  29116  atssma  29125  atomli  29129  atoml2i  29130  atordi  29131  atcvatlem  29132  chirredlem1  29137  chirredlem2  29138  chirredlem3  29139  atcvat4i  29144  atabsi  29148  mdsymlem1  29150  dmdbr6ati  29170  cdj3lem3  29185  inin  29241  difeq  29243  difuncomp  29256  disjdifprg  29274  iundisj2f  29289  disjunsn  29293  imadifxp  29300  fnresin  29315  df1stres  29365  df2ndres  29366  padct  29381  iocinif  29428  difioo  29429  iundisj2fi  29439  xrge00  29513  xrge0slmod  29671  lmxrge0  29822  esumrnmpt2  29953  esumpfinvallem  29959  ldgenpisyslem1  30049  ldgenpisys  30052  measxun2  30096  measunl  30102  carsgclctunlem1  30202  carsgclctunlem2  30204  eulerpartlemt  30256  eulerpartgbij  30257  probmeasb  30315  bayesth  30324  ballotlemfp1  30376  ballotlemfval0  30380  signstres  30474  subfacp1lem3  30925  subfacp1lem5  30927  pconnconn  30974  cvmscld  31016  cvmsss2  31017  mrsubvrs  31180  mthmpps  31240  frind  31494  frrlem5  31538  cldbnd  32016  bj-inrab3  32625  bj-2upln1upl  32712  bj-sscon  32714  bj-rest0  32736  bj-diagval  32762  icoreclin  32876  fin2so  33067  ptrest  33079  poimirlem3  33083  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem14  33094  poimirlem15  33095  poimirlem16  33096  poimirlem18  33098  poimirlem19  33099  poimirlem21  33101  poimirlem22  33102  poimirlem27  33107  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  cnambfre  33129  asindmre  33166  dvasin  33167  dvreasin  33169  dvreacos  33170  sstotbnd2  33244  bndss  33256  l1cvat  33861  pmod2iN  34654  pmodN  34655  pmodl42N  34656  osumcllem3N  34763  osumcllem4N  34764  dihmeetlem19N  36133  dihmeetALTN  36135  elrfi  36776  diophrw  36841  eldioph2lem1  36842  eldioph2lem2  36843  diophin  36855  diophren  36896  dnwech  37137  fnwe2lem2  37140  kelac1  37152  kelac2lem  37153  kelac2  37154  lmhmlnmsplit  37176  pwssplit4  37178  pwfi2f1o  37185  proot1hash  37298  rp-fakeuninass  37382  elcnvcnvintab  37408  relintab  37409  elcnvcnvlem  37425  conrel1d  37475  dfrcl2  37486  iunrelexp0  37514  ntrk0kbimka  37858  neicvgbex  37931  hashnzfz  38040  zfregs2VD  38598  iunconnlem2  38693  ssinss2d  38750  restuni4  38829  restuni6  38830  iccdifioo  39187  uzinico2  39235  sumnnodd  39298  limsupvaluz  39376  cncfuni  39434  fouriersw  39785  saliincl  39882  iundjiunlem  40013  iundjiun  40014  caragenuncllem  40063  caragendifcl  40065  isomenndlem  40081  hoidmvlelem2  40147  smflimlem1  40316  perfectALTVlem2  40956  rnghmsscmap2  41291  rnghmsubcsetclem1  41293  rnghmsubcsetc  41295  rngccat  41296  rngcid  41297  rngchomrnghmresALTV  41314  rngcifuestrc  41315  funcrngcsetc  41316  rhmsscmap2  41337  rhmsubcsetclem1  41339  rhmsubcsetc  41341  ringccat  41342  ringcid  41343  rhmsscrnghm  41344  rhmsubcrngclem1  41345  rhmsubcrngc  41347  rngcresringcat  41348  funcringcsetc  41353  rngcrescrhm  41403  rhmsubclem3  41406  rhmsubc  41408  rngcrescrhmALTV  41421  rhmsubcALTVlem3  41424  rhmsubcALTVlem4  41425
  Copyright terms: Public domain W3C validator