Theorem inteqd 4291

Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
inteqd.1

Assertion

Ref	Expression
inteqd

Proof of Theorem inteqd

Step	Hyp	Ref	Expression
1		inteqd.1	. 2
2		inteq 4289	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  |^|cint 4286

This theorem is referenced by:  intprg  4321  ordintdif  4932  elreldm  5232  fniinfv  5932  onsucmin  6656  elxp5  6745  1stval2  6817  2ndval2  6818  fundmen  7609  xpsnen  7621  unblem2  7793  unblem3  7794  fiint  7817  elfi2  7894  fi0  7900  elfiun  7910  tcvalg  8190  tz9.12lem3  8228  rankvalb  8236  rankvalg  8256  ranksnb  8266  rankonidlem  8267  cardval3  8354  cardidm  8361  cfval  8648  cflim3  8663  coftr  8674  isfin3ds  8730  fin23lem17  8739  fin23lem39  8751  isf33lem  8767  isf34lem5  8779  isf34lem6  8781  wuncval  9141  tskmval  9238  xpnnenOLD  13943  mrcfval  15005  mrcval  15007  cycsubg2  16238  efgval  16735  lspfval  17619  lspval  17621  lsppropd  17664  aspval  17977  aspval2  17996  clsfval  19526  clsval  19538  clsval2  19551  hauscmplem  19906  cmpfi  19908  1stcfb  19946  fclscmp  20531  spanval  26251  chsupid  26330  sigagenval  28140  kur14  28660  mclsval  28923  dfrtrcl2  29071  igenval  30458  mzpval  30664  dnnumch3lem  30992  aomclem8  31007  rgspnval  31117  iotain  31324  pclfvalN  35613  pclvalN  35614  diaintclN  36785  docaffvalN  36848  docafvalN  36849  docavalN  36850  dibintclN  36894  dihglb2  37069  dihintcl  37071

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-ral 2812  df-int 4287