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

Theorem inteqi 3882
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 3881 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2ax-mp 8 1  |-  |^| A  =  |^| B
Colors of variables: wff set class
Syntax hints:    = wceq 1632   |^|cint 3878
This theorem is referenced by:  elintrab  3890  ssintrab  3901  intmin2  3905  intsng  3913  intexrab  4186  intabs  4188  ordintdif  4457  op1stb  4585  bm2.5ii  4613  dfiin3g  4948  op2ndb  5172  knatar  5873  oawordeulem  6568  oeeulem  6615  iinfi  7187  tcsni  7444  rankval2  7506  rankval3b  7514  cf0  7893  cfval2  7902  cofsmo  7911  isf34lem4  8019  isf34lem7  8021  sstskm  8480  dfnn3  9776  cycsubg  14661  efgval2  15049  00lsp  15754  alexsublem  17754  intopcoaconb  25643  imaiinfv  26862  elrfi  26872
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