MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inteqd Structured version   Unicode version

Theorem inteqd 4276
Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
inteqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
inteqd  |-  ( ph  ->  |^| A  =  |^| B )

Proof of Theorem inteqd
StepHypRef Expression
1 inteqd.1 . 2  |-  ( ph  ->  A  =  B )
2 inteq 4274 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 16 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383   |^|cint 4271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-int 4272
This theorem is referenced by:  intprg  4306  ordintdif  4917  elreldm  5217  fniinfv  5917  onsucmin  6641  elxp5  6730  1stval2  6802  2ndval2  6803  fundmen  7591  xpsnen  7603  unblem2  7775  unblem3  7776  fiint  7799  elfi2  7876  fi0  7882  elfiun  7892  tcvalg  8172  tz9.12lem3  8210  rankvalb  8218  rankvalg  8238  ranksnb  8248  rankonidlem  8249  cardval3  8336  cardidm  8343  cfval  8630  cflim3  8645  coftr  8656  isfin3ds  8712  fin23lem17  8721  fin23lem39  8733  isf33lem  8749  isf34lem5  8761  isf34lem6  8763  wuncval  9123  tskmval  9220  xpnnenOLD  13924  mrcfval  14986  mrcval  14988  cycsubg2  16216  efgval  16713  lspfval  17597  lspval  17599  lsppropd  17642  aspval  17955  aspval2  17974  clsfval  19503  clsval  19515  clsval2  19528  hauscmplem  19883  cmpfi  19885  1stcfb  19923  fclscmp  20508  spanval  26227  chsupid  26306  sigagenval  28117  kur14  28637  mclsval  28900  dfrtrcl2  29048  igenval  30433  mzpval  30639  dnnumch3lem  30967  aomclem8  30982  rgspnval  31093  iotain  31278  pclfvalN  35353  pclvalN  35354  diaintclN  36525  docaffvalN  36588  docafvalN  36589  docavalN  36590  dibintclN  36634  dihglb2  36809  dihintcl  36811
  Copyright terms: Public domain W3C validator