Theorem incom 3690

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.

Step	Hyp	Ref	Expression
1		ancom 450	. . 3
2		elin 3686	. . 3
3		elin 3686	. . 3
4	1, 2, 3	3bitr4i 277	. 2
5	4	eqriv 2453	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  i^icin 3474

This theorem is referenced by:  ineq2  3693  dfss1  3702  in12  3708  in32  3709  in13  3710  in31  3711  inss2  3718  sslin  3723  inss  3726  indif1  3741  indifcom  3742  indir  3745  symdif1  3762  dfrab2  3773  disjr  3868  ssdifin0  3909  difdifdir  3915  uneqdifeq  3916  diftpsn3  4168  iinrab2  4393  iunin1  4395  iinin1  4401  riinn0  4405  rintn0  4421  disjprg  4448  disjxun  4450  inex2  4594  ordtri3or  4915  resiun1  5297  dmres  5299  rescom  5303  resima2  5312  xpssres  5313  resindm  5323  resdmdfsn  5324  resopab  5325  imadisj  5361  ndmima  5378  intirr  5390  djudisj  5439  imainrect  5453  dmresv  5470  resdmres  5503  coeq0  5521  fnresdisj  5696  fnimaeq0  5707  resasplit  5760  fresaun  5761  fresaunres2  5762  fresaunres1  5763  f0rn0  5775  fvun2  5945  fveqressseq  6027  ressnop0  6078  fninfp  6098  fvsnun1  6106  fsnunfv  6111  fnsuppeq0OLD  6132  fveqf1o  6205  orduniss2  6668  offres  6795  curry1  6892  curry2  6895  fpar  6904  fnsuppeq0  6947  smores3  7043  oacomf1o  7233  ralxpmap  7488  difsnen  7619  domunsncan  7637  domunsn  7687  limensuci  7713  phplem2  7717  pssnn  7758  dif1enOLD  7772  dif1en  7773  domunfican  7813  marypha1lem  7913  dfsup2OLD  7923  dfsup3OLD  7924  epfrs  8183  zfregs2  8185  tskwe  8352  dif1card  8409  dfac8b  8433  ac10ct  8436  kmlem11  8561  kmlem12  8562  cdacomen  8582  onacda  8598  ackbij1lem14  8634  ackbij1lem16  8636  ackbij1lem18  8638  fin23lem26  8726  fin23lem19  8737  fin23lem30  8743  isf32lem4  8757  isf34lem7  8780  isf34lem6  8781  axdc3lem4  8854  brdom7disj  8930  brdom6disj  8931  fpwwe2lem13  9041  canthp1lem1  9051  grothprim  9233  fzpreddisj  11758  fzdifsuc  11768  fseq1p1m1  11781  hashgval  12408  hashun3  12452  hashfun  12495  hashbclem  12501  limsupgle  13300  prmreclem2  14435  setsid  14673  ressinbas  14693  wunress  14696  mreexexlem2d  15042  mreexexlem4d  15044  oppcinv  15170  cnvps  15842  pmtrmvd  16481  lsmmod2  16694  lsmdisj3  16701  lsmdisjr  16702  lsmdisj2r  16703  lsmdisj3r  16704  lsmdisj2a  16705  lsmdisj2b  16706  lsmdisj3a  16707  lsmdisj3b  16708  subgdisj2  16710  pj2f  16716  pj1id  16717  frgpuplem  16790  gsummptfzsplitl  16953  dprd2da  17091  dmdprdsplit2lem  17094  dmdprdsplit2  17095  pgpfaclem1  17132  lmhmlsp  17695  pwssplit1  17705  ltbwe  18137  psrbag0  18159  psgndiflemB  18636  pjpm  18739  islindf4  18873  indistopon  19502  fctop  19505  cctop  19507  elcls  19574  mretopd  19593  restin  19667  restsn  19671  restcld  19673  neitr  19681  resstopn  19687  lecldbas  19720  nrmsep  19858  regsep2  19877  isreg2  19878  ordthaus  19885  cmpsublem  19899  cmpsub  19900  hauscmplem  19906  bwth  19910  bwthOLD  19911  iuncon  19929  cldllycmp  19996  kgentopon  20039  llycmpkgen2  20051  1stckgen  20055  txkgen  20153  kqcldsat  20234  regr1lem2  20241  fbun  20341  fin1aufil  20433  fclsfnflim  20528  ustexsym  20718  restutopopn  20741  ustuqtop5  20748  ressuss  20766  metreslem  20865  blcld  21008  ressxms  21028  ressms  21029  restmetu  21090  reconn  21333  metdseq0  21358  metnrmlem3  21365  unmbl  21948  volun  21955  volinun  21956  iundisj2  21959  icombl  21974  ioombl  21975  uniioombllem2  21992  uniioombllem4  21995  dyaddisjlem  22004  dyaddisj  22005  mbfconstlem  22036  mbfeqalem  22049  ismbf3d  22061  itg1addlem5  22107  itgsplitioo  22244  lhop  22417  tdeglem4  22458  vieta1lem2  22707  xrlimcnp  23298  chtdif  23432  ppidif  23437  ppi1  23438  cht1  23439  perfectlem2  23505  rplogsum  23712  perpcom  24090  cusgrasizeindslem2  24474  ex-dif  25144  ococi  26323  orthin  26364  lediri  26455  pjoml2i  26503  pjoml4i  26505  cmcmlem  26509  cmbr3i  26518  cmm2i  26525  cm0  26527  fh1  26536  fh2  26537  cm2j  26538  qlaxr3i  26554  pjclem2  27115  stm1ri  27163  golem1  27190  dmdbr5  27227  mddmd2  27228  cvmdi  27243  mdsldmd1i  27250  csmdsymi  27253  mdexchi  27254  cvexchi  27288  atssma  27297  atomli  27301  atoml2i  27302  atordi  27303  atcvatlem  27304  chirredlem1  27309  chirredlem2  27310  chirredlem3  27311  atcvat4i  27316  atabsi  27320  mdsymlem1  27322  dmdbr6ati  27342  cdj3lem3  27357  inin  27413  difeq  27416  disjdifprg  27436  iundisj2f  27449  disjunsn  27453  imadifxp  27458  fnresin  27470  ofpreima2  27508  df1stres  27522  df2ndres  27523  iocinif  27592  difioo  27593  iundisj2fi  27602  xrge00  27674  xrge0slmod  27834  ordtconlem1  27906  lmxrge0  27934  esumpfinvallem  28080  measxun2  28181  measvuni  28185  measunl  28187  measinb  28192  eulerpartlemt  28310  eulerpartgbij  28311  probmeasb  28369  cndprobnul  28376  bayesth  28378  ballotlemfp1  28430  ballotlemfval0  28434  ballotlemgun  28463  signstres  28532  subfacp1lem3  28626  subfacp1lem5  28628  pconcon  28676  cvmscld  28718  cvmsss2  28719  mrsubvrs  28882  mthmpps  28942  dfpred3  29254  epsetlike  29274  pred0  29279  wfi  29287  frind  29323  wfrlem5  29347  frrlem5  29391  nofulllem5  29466  fin2so  30040  ptrest  30048  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  cnambfre  30063  asindmre  30102  dvasin  30103  dvreasin  30105  dvreacos  30106  cldbnd  30144  sstotbnd2  30270  bndss  30282  elrfi  30626  diophrw  30692  eldioph2lem1  30693  eldioph2lem2  30694  diophin  30706  diophren  30747  dnwech  30994  fnwe2lem2  30997  kelac1  31009  kelac2lem  31010  kelac2  31011  lmhmlnmsplit  31033  pwssplit4  31035  pwfi2f1o  31044  proot1hash  31160  hashnzfz  31225  iccdifioo  31555  sumnnodd  31636  cncfuni  31689  fouriersw  32014  rnghmsscmap2  32781  rnghmsubcsetclem1  32783  rnghmsubcsetc  32785  rngccat  32786  rngcid  32787  rngchomrnghmresOLD  32804  rngcifuestrc  32805  funcrngcsetc  32806  rhmsscmap2  32827  rhmsubcsetclem1  32829  rhmsubcsetc  32831  ringccat  32832  ringcid  32833  rhmsscrnghm  32834  rhmsubcrngclem1  32835  rhmsubcrngc  32837  rngcresringcat  32838  funcringcsetc  32843  rngcrescrhm  32893  rhmsubclem3  32896  rhmsubc  32898  rngcrescrhmOLD  32912  rhmsubcOLDlem3  32915  rhmsubcOLDlem4  32916  zfregs2VD  33641  iunconlem2  33735  bj-2upln1upl  34582  bj-diagval  34605  l1cvat  34780  pmod2iN  35573  pmodN  35574  pmodl42N  35575  osumcllem3N  35682  osumcllem4N  35683  dihmeetlem19N  37052  dihmeetALTN  37054  rp-fakeuninass  37741  conrel1d  37761  xpcoidgend  37774  cotr2  37787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482