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

Theorem inteqd 3883
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 3881 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2syl 15 1  |-  ( ph  ->  |^| A  =  |^| B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   |^|cint 3878
This theorem is referenced by:  intprg  3912  ordintdif  4457  onsucmin  4628  elreldm  4919  elxp5  5177  fniinfv  5597  1stval2  6153  2ndval2  6154  fundmen  6950  xpsnen  6962  unblem2  7126  unblem3  7127  fiint  7149  elfi2  7184  fi0  7189  elfiun  7199  tcvalg  7439  tz9.12lem3  7477  rankvalb  7485  rankvalg  7505  ranksnb  7515  rankonidlem  7516  cardval3  7601  cardidm  7608  cfval  7889  cflim3  7904  coftr  7915  isfin3ds  7971  fin23lem17  7980  fin23lem39  7992  isf33lem  8008  isf34lem5  8020  isf34lem6  8022  wuncval  8380  tskmval  8477  xpnnenOLD  12504  mrcfval  13526  mrcval  13528  cycsubg2  14670  efgval  15042  lspfval  15746  lspval  15748  lsppropd  15791  aspval  16084  aspval2  16102  clsfval  16778  clsval  16790  clsval2  16803  hauscmplem  17149  cmpfi  17151  1stcfb  17187  fclscmp  17741  spanval  21928  chsupid  22007  sigagenval  23516  kur14  23762  dfrtrcl2  24060  moec  25150  istopx  25650  istopxc  25651  indcls2  26099  igenval  26789  mzpval  26913  dnnumch3lem  27246  aomclem8  27262  rgspnval  27476  iotain  27720  pclfvalN  30700  pclvalN  30701  diaintclN  31870  docaffvalN  31933  docafvalN  31934  docavalN  31935  dibintclN  31979  dihglb2  32154  dihintcl  32156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-int 3879
  Copyright terms: Public domain W3C validator