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

Theorem inteqi 4275
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 4274 . 2  |-  ( A  =  B  ->  |^| A  =  |^| B )
31, 2ax-mp 5 1  |-  |^| A  =  |^| B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   |^|cint 4271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-int 4272
This theorem is referenced by:  elintrab  4283  ssintrab  4295  intmin2  4299  intsng  4307  intexrab  4596  intabs  4598  op1stb  4707  ordintdif  4916  dfiin3g  5245  op2ndb  5475  knatar  6228  bm2.5ii  6614  oawordeulem  7195  oeeulem  7242  iinfi  7869  tcsni  8165  rankval2  8227  rankval3b  8235  cf0  8622  cfval2  8631  cofsmo  8640  isf34lem4  8748  isf34lem7  8750  sstskm  9209  dfnn3  10545  trclun  12932  cycsubg  16428  efgval2  16941  00lsp  17822  alexsublem  20710  imaiinfv  30865  elrfi  30866  dfrcl2  38193
  Copyright terms: Public domain W3C validator