Theorem inidm 3706

Description: Idempotent law for intersection of classes. Theorem 15 of [Suppes] p. 26. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
inidm

Proof of Theorem inidm

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		anidm 644	. 2
2	1	ineqri 3691	1

Syntax hints:  =wceq 1395  e.wcel 1818  i^icin 3474

This theorem is referenced by:  inindi  3714  inindir  3715  uneqin  3748  ssdifeq0  3910  intsng  4322  xpindi  5141  xpindir  5142  resindm  5323  fnfvof  6553  ofres  6555  offval2  6556  ofrfval2  6557  suppssof1OLD  6559  ofco  6560  offveq  6561  offveqb  6562  ofc1  6563  ofc2  6564  caofref  6566  caofrss  6573  caoftrn  6575  suppssof1  6952  suppofss1d  6956  suppofss2d  6957  fisn  7907  dffi3  7911  ofsubeq0  10558  ofnegsub  10559  ofsubge0  10560  seqof  12164  incexc  13649  sadeq  14122  smuval2  14132  smumul  14143  ressinbas  14693  pwsle  14889  pwsleval  14890  ghmplusg  16852  gsumzaddlem  16934  gsumzadd  16935  gsumzaddlemOLD  16936  gsumzaddOLD  16937  lcomf  17548  lcomfsupp  17550  crng2idl  17887  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrbagaddcl  18020  psrbagaddclOLD  18021  psrbagcon  18022  psrbaglefi  18023  psrbaglefiOLD  18024  psrbagconf1o  18026  gsumbagdiaglem  18027  psraddcl  18036  psrvscacl  18046  psrlidm  18056  psrlidmOLD  18057  psrdi  18061  psrdir  18062  mplsubglem  18093  mplsubglemOLD  18095  psrbagev1  18177  psrbagev1OLD  18178  evlslem3  18183  evlslem1  18184  psrplusgpropd  18277  coe1add  18305  pf1ind  18391  frlmipval  18810  frlmphllem  18811  frlmphl  18812  frlmsslsp  18829  frlmsslspOLD  18830  frlmup1  18832  mndvcl  18893  matplusgcell  18935  matsubgcell  18936  mat1dimscm  18977  baspartn  19455  indistopon  19502  epttop  19510  dissnlocfin  20030  ptbasin  20078  snfil  20365  tsmsadd  20649  ust0  20722  ustuqtop1  20744  rrxcph  21824  rrxds  21825  volun  21955  mbfmulc2lem  22054  mbfaddlem  22067  0pledm  22080  i1faddlem  22100  i1fmullem  22101  i1fadd  22102  i1fmul  22103  itg1addlem4  22106  i1fmulclem  22109  i1fmulc  22110  itg1lea  22119  itg1le  22120  mbfi1fseqlem5  22126  mbfi1flimlem  22129  mbfmullem2  22131  xrge0f  22138  itg2ge0  22142  itg2lea  22151  itg2mulclem  22153  itg2mulc  22154  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2mono  22160  itg2i1fseqle  22161  itg2i1fseq  22162  itg2addlem  22165  itg2cnlem1  22168  dvaddf  22345  dvmulf  22346  dvcmulf  22348  dv11cn  22402  plyaddlem1  22610  plyaddlem  22612  coeeulem  22621  coeaddlem  22646  coemulc  22652  dgradd2  22665  dgrcolem2  22671  ofmulrt  22678  plydivlem3  22691  plydivlem4  22692  plydiveu  22694  plyrem  22701  vieta1lem2  22707  elqaalem3  22717  qaa  22719  jensenlem2  23317  jensen  23318  basellem7  23360  basellem9  23362  dchrmulcl  23524  chssoc  26414  chjidm  26438  mdslmd3i  27251  inin  27413  disjnf  27433  ofrn  27479  ofrn2  27480  ofresid  27482  offval2f  27506  gsumle  27770  hauseqcn  27877  ofcof  28106  sibfof  28282  ofccat  28497  plymul02  28503  signshf  28545  msrid  28905  nepss  29095  predidm  29268  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  ftc1anclem3  30092  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem8  30097  blbnd  30283  mzpclall  30659  mzpindd  30678  dgrsub2  31084  mpaaeu  31099  mendring  31141  caofcan  31228  ofmul12  31230  ofdivrec  31231  ofdivcan4  31232  ofdivdiv2  31233  expgrowth  31240  binomcxplemrat  31255  binomcxplemnotnn0  31261  dvsinax  31708  dvcosax  31723  dvdivcncf  31724  uzlidlring  32735  ofaddmndmap  32933  mndpsuppss  32964  mndpfsupp  32969  dmatALTbas  33002  dflinc2  33011  aacllem  33216  bj-inrab2  34496  lshpinN  34714  lfladdcl  34796  lflvscl  34802  ldualvaddval  34856  lclkrlem2e  37238

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