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

Theorem inteqd 4136
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 4134 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 16 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369   |^|cint 4131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ral 2723  df-int 4132
This theorem is referenced by:  intprg  4165  ordintdif  4771  elreldm  5067  fniinfv  5753  onsucmin  6435  elxp5  6526  1stval2  6597  2ndval2  6598  fundmen  7386  xpsnen  7398  unblem2  7568  unblem3  7569  fiint  7591  elfi2  7667  fi0  7673  elfiun  7683  tcvalg  7961  tz9.12lem3  7999  rankvalb  8007  rankvalg  8027  ranksnb  8037  rankonidlem  8038  cardval3  8125  cardidm  8132  cfval  8419  cflim3  8434  coftr  8445  isfin3ds  8501  fin23lem17  8510  fin23lem39  8522  isf33lem  8538  isf34lem5  8550  isf34lem6  8552  wuncval  8912  tskmval  9009  xpnnenOLD  13495  mrcfval  14549  mrcval  14551  cycsubg2  15721  efgval  16217  lspfval  17057  lspval  17059  lsppropd  17102  aspval  17402  aspval2  17420  clsfval  18632  clsval  18644  clsval2  18657  hauscmplem  19012  cmpfi  19014  1stcfb  19052  fclscmp  19606  spanval  24739  chsupid  24818  sigagenval  26586  kur14  27107  dfrtrcl2  27353  igenval  28864  mzpval  29071  dnnumch3lem  29402  aomclem8  29417  rgspnval  29528  iotain  29674  pclfvalN  33536  pclvalN  33537  diaintclN  34706  docaffvalN  34769  docafvalN  34770  docavalN  34771  dibintclN  34815  dihglb2  34990  dihintcl  34992
  Copyright terms: Public domain W3C validator