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

Theorem incom 3763
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 464 . . 3 ((𝑥𝐴𝑥𝐵) ↔ (𝑥𝐵𝑥𝐴))
2 elin 3754 . . 3 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
3 elin 3754 . . 3 (𝑥 ∈ (𝐵𝐴) ↔ (𝑥𝐵𝑥𝐴))
41, 2, 33bitr4i 290 . 2 (𝑥 ∈ (𝐴𝐵) ↔ 𝑥 ∈ (𝐵𝐴))
54eqriv 2603 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 382   = wceq 1474  wcel 1976  cin 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543
This theorem is referenced by:  ineq2  3766  sseqin2  3775  dfss1OLD  3776  in12  3782  in32  3783  in13  3784  in31  3785  inss2  3792  sslin  3797  inss  3800  indif1  3826  indifcom  3827  indir  3830  dfsymdif3  3848  dfrab2  3858  0in  3917  disjr  3966  ssdifin0  3998  difdifdir  4004  uneqdifeq  4005  uneqdifeqOLD  4006  diftpsn3OLD  4270  iinrab2  4510  iunin1  4512  iinin1  4518  riinn0  4522  disjprg  4569  disjxun  4572  inex2  4720  resiun1OLD  5321  dmres  5323  rescom  5327  resima2OLD  5337  resindm  5348  resdmdfsn  5349  resopab  5350  imadisj  5387  intirr  5417  djudisj  5463  imainrect  5477  dmresv  5494  resdmres  5526  coeq0  5544  dfpred3  5590  wfi  5613  ordtri3or  5655  fnresdisj  5898  fnimaeq0  5909  resasplit  5969  fresaun  5970  fresaunres2  5971  fresaunres1  5972  f0rn0  5985  fvun2  6162  fveqressseq  6245  ressnop0  6300  fninfp  6320  fvsnun1  6328  fsnunfv  6333  fveqf1o  6432  orduniss2  6899  offres  7028  curry1  7130  curry2  7133  fpar  7142  wfrlem5  7280  smores3  7311  oacomf1o  7506  ralxpmap  7767  difsnen  7901  domunsncan  7919  domunsn  7969  limensuci  7995  phplem2  7999  pssnn  8037  dif1en  8052  domunfican  8092  marypha1lem  8196  zfregfr  8366  epfrs  8464  zfregs2  8466  tskwe  8633  dif1card  8690  dfac8b  8711  ac10ct  8714  kmlem11  8839  kmlem12  8840  cdacomen  8860  onacda  8876  ackbij1lem14  8912  ackbij1lem16  8914  ackbij1lem18  8916  fin23lem26  9004  fin23lem19  9015  fin23lem30  9021  isf32lem4  9035  isf34lem7  9058  isf34lem6  9059  axdc3lem4  9132  brdom7disj  9208  brdom6disj  9209  fpwwe2lem13  9317  canthp1lem1  9327  grothprim  9509  fzpreddisj  12212  fzdifsuc  12222  fseq1p1m1  12235  hashgval  12934  hashun3  12983  hashfun  13033  hashbclem  13042  xpcoidgend  13505  cotr2  13507  limsupgle  13999  prmreclem2  15402  setsdm  15667  setsfun  15668  setsfun0  15669  setsid  15685  ressinbas  15706  wunress  15710  mreexexlem2d  16071  mreexexlem4d  16073  oppcinv  16206  cnvps  16978  pmtrmvd  17642  lsmmod2  17855  lsmdisj3  17862  lsmdisjr  17863  lsmdisj2r  17864  lsmdisj3r  17865  lsmdisj2a  17866  lsmdisj2b  17867  lsmdisj3a  17868  lsmdisj3b  17869  subgdisj2  17871  pj2f  17877  pj1id  17878  frgpuplem  17951  gsummptfzsplitl  18099  dprd2da  18207  dmdprdsplit2lem  18210  dmdprdsplit2  18211  pgpfaclem1  18246  lmhmlsp  18813  pwssplit1  18823  ltbwe  19236  psrbag0  19258  psgndiflemB  19707  pjpm  19810  islindf4  19935  elcls  20626  mretopd  20645  restin  20719  restcld  20725  neitr  20733  resstopn  20739  lecldbas  20772  nrmsep  20910  regsep2  20929  isreg2  20930  ordthaus  20937  cmpsublem  20951  cmpsub  20952  hauscmplem  20958  bwth  20962  iuncon  20980  cldllycmp  21047  kgentopon  21090  llycmpkgen2  21102  1stckgen  21106  txkgen  21204  kqcldsat  21285  regr1lem2  21292  fbun  21393  fin1aufil  21485  fclsfnflim  21580  ustexsym  21768  restutopopn  21791  ustuqtop5  21798  ressuss  21816  metreslem  21915  blcld  22058  ressxms  22078  ressms  22079  restmetu  22123  reconn  22368  metdseq0  22393  metnrmlem3  22400  unmbl  23026  volun  23034  volinun  23035  iundisj2  23038  icombl  23053  ioombl  23054  uniioombllem2  23071  uniioombllem4  23074  dyaddisjlem  23083  dyaddisj  23084  mbfconstlem  23116  mbfeqalem  23129  ismbf3d  23141  itg1addlem5  23187  itgsplitioo  23324  lhop  23497  tdeglem4  23538  vieta1lem2  23784  xrlimcnp  24409  perfectlem2  24669  rplogsum  24930  perpcom  25323  cusgrasizeindslem1  25765  ex-dif  26435  ococi  27451  orthin  27492  lediri  27583  pjoml2i  27631  pjoml4i  27633  cmcmlem  27637  cmbr3i  27646  cmm2i  27653  cm0  27655  fh1  27664  fh2  27665  cm2j  27666  qlaxr3i  27682  pjclem2  28242  stm1ri  28290  golem1  28317  dmdbr5  28354  mddmd2  28355  cvmdi  28370  mdsldmd1i  28377  csmdsymi  28380  mdexchi  28381  cvexchi  28415  atssma  28424  atomli  28428  atoml2i  28429  atordi  28430  atcvatlem  28431  chirredlem1  28436  chirredlem2  28437  chirredlem3  28438  atcvat4i  28443  atabsi  28447  mdsymlem1  28449  dmdbr6ati  28469  cdj3lem3  28484  inin  28540  difeq  28542  difuncomp  28555  disjdifprg  28573  iundisj2f  28588  disjunsn  28592  imadifxp  28599  fnresin  28615  df1stres  28667  df2ndres  28668  padct  28688  iocinif  28736  difioo  28737  iundisj2fi  28746  xrge00  28820  xrge0slmod  28978  lmxrge0  29129  esumrnmpt2  29260  esumpfinvallem  29266  ldgenpisyslem1  29356  ldgenpisys  29359  measxun2  29403  measunl  29409  carsgclctunlem1  29509  carsgclctunlem2  29511  eulerpartlemt  29563  eulerpartgbij  29564  probmeasb  29622  bayesth  29631  ballotlemfp1  29683  ballotlemfval0  29687  signstres  29781  subfacp1lem3  30221  subfacp1lem5  30223  pconcon  30270  cvmscld  30312  cvmsss2  30313  mrsubvrs  30476  mthmpps  30536  frind  30787  frrlem5  30831  nofulllem5  30908  cldbnd  31294  bj-inrab3  31917  bj-2upln1upl  32005  bj-rest0  32027  bj-diagval  32067  icoreclin  32181  fin2so  32366  ptrest  32378  poimirlem3  32382  poimirlem11  32390  poimirlem12  32391  poimirlem13  32392  poimirlem14  32393  poimirlem15  32394  poimirlem16  32395  poimirlem18  32397  poimirlem19  32398  poimirlem21  32400  poimirlem22  32401  poimirlem27  32406  mblfinlem3  32418  mblfinlem4  32419  ismblfin  32420  cnambfre  32428  asindmre  32465  dvasin  32466  dvreasin  32468  dvreacos  32469  sstotbnd2  32543  bndss  32555  l1cvat  33160  pmod2iN  33953  pmodN  33954  pmodl42N  33955  osumcllem3N  34062  osumcllem4N  34063  dihmeetlem19N  35432  dihmeetALTN  35434  elrfi  36075  diophrw  36140  eldioph2lem1  36141  eldioph2lem2  36142  diophin  36154  diophren  36195  dnwech  36436  fnwe2lem2  36439  kelac1  36451  kelac2lem  36452  kelac2  36453  lmhmlnmsplit  36475  pwssplit4  36477  pwfi2f1o  36484  proot1hash  36597  rp-fakeuninass  36681  elcnvcnvintab  36707  relintab  36708  elcnvcnvlem  36724  conrel1d  36774  dfrcl2  36785  iunrelexp0  36813  ntrkbimka  37156  ntrk0kbimka  37157  neicvgbex  37230  hashnzfz  37341  zfregs2VD  37898  iunconlem2  37993  ssinss2d  38053  restuni4  38136  restuni6  38137  iccdifioo  38389  sumnnodd  38498  cncfuni  38573  fouriersw  38925  saliincl  39022  iundjiunlem  39153  iundjiun  39154  caragenuncllem  39203  caragendifcl  39205  isomenndlem  39221  hoidmvlelem2  39287  smflimlem1  39458  perfectALTVlem2  39967  prinfzo0  40187  rnghmsscmap2  41764  rnghmsubcsetclem1  41766  rnghmsubcsetc  41768  rngccat  41769  rngcid  41770  rngchomrnghmresALTV  41787  rngcifuestrc  41788  funcrngcsetc  41789  rhmsscmap2  41810  rhmsubcsetclem1  41812  rhmsubcsetc  41814  ringccat  41815  ringcid  41816  rhmsscrnghm  41817  rhmsubcrngclem1  41818  rhmsubcrngc  41820  rngcresringcat  41821  funcringcsetc  41826  rngcrescrhm  41876  rhmsubclem3  41879  rhmsubc  41881  rngcrescrhmALTV  41895  rhmsubcALTVlem3  41898  rhmsubcALTVlem4  41899
  Copyright terms: Public domain W3C validator