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

Theorem inteqi 4216
Description: Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
inteqi.1  |-  A  =  B
Assertion
Ref Expression
inteqi  |-  |^| A  =  |^| B

Proof of Theorem inteqi
StepHypRef Expression
1 inteqi.1 . 2  |-  A  =  B
2 inteq 4215 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2ax-mp 5 1  |-  |^| A  =  |^| B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   |^|cint 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ral 2797  df-int 4213
This theorem is referenced by:  elintrab  4224  ssintrab  4235  intmin2  4239  intsng  4247  intexrab  4535  intabs  4537  op1stb  4646  ordintdif  4852  dfiin3g  5177  op2ndb  5407  knatar  6133  bm2.5ii  6503  oawordeulem  7079  oeeulem  7126  iinfi  7754  tcsni  8050  rankval2  8112  rankval3b  8120  cf0  8507  cfval2  8516  cofsmo  8525  isf34lem4  8633  isf34lem7  8635  sstskm  9096  dfnn3  10423  cycsubg  15797  efgval2  16311  00lsp  17154  alexsublem  19718  imaiinfv  29153  elrfi  29154
  Copyright terms: Public domain W3C validator