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

Theorem inteqi 3866
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 3865 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2ax-mp 8 1  |-  |^| A  =  |^| B
Colors of variables: wff set class
Syntax hints:    = wceq 1623   |^|cint 3862
This theorem is referenced by:  elintrab  3874  ssintrab  3885  intmin2  3889  intsng  3897  intexrab  4170  intabs  4172  ordintdif  4441  op1stb  4569  bm2.5ii  4597  dfiin3g  4932  op2ndb  5156  knatar  5857  oawordeulem  6552  oeeulem  6599  iinfi  7171  tcsni  7428  rankval2  7490  rankval3b  7498  cf0  7877  cfval2  7886  cofsmo  7895  isf34lem4  8003  isf34lem7  8005  sstskm  8464  dfnn3  9760  cycsubg  14645  efgval2  15033  00lsp  15738  alexsublem  17738  intopcoaconb  25540  imaiinfv  26759  elrfi  26769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-int 3863
  Copyright terms: Public domain W3C validator