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

Theorem inteqi 4883
Description: Equality inference for class intersection. (Contributed by NM, 2-Sep-2003.)
Hypothesis
Ref Expression
inteqi.1 𝐴 = 𝐵
Assertion
Ref Expression
inteqi 𝐴 = 𝐵

Proof of Theorem inteqi
StepHypRef Expression
1 inteqi.1 . 2 𝐴 = 𝐵
2 inteq 4882 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539   cint 4879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-ral 3069  df-int 4880
This theorem is referenced by:  elintrab  4891  ssintrab  4902  intmin2  4906  intsng  4916  intexrab  5264  intabs  5266  op1stb  5386  dfiin3g  5874  op2ndb  6130  ordintdif  6315  knatar  7228  uniordint  7651  oawordeulem  8385  oeeulem  8432  iinfi  9176  dfttrcl2  9482  tcsni  9501  rankval2  9576  rankval3b  9584  cf0  10007  cfval2  10016  cofsmo  10025  isf34lem4  10133  isf34lem7  10135  sstskm  10598  dfnn3  11987  trclun  14725  cycsubg  18827  efgval2  19330  00lsp  20243  alexsublem  23195  intimafv  31043  dynkin  32135  noextendlt  33872  nosepne  33883  nosepdm  33887  nosupbnd2lem1  33918  noinfbnd2lem1  33933  noetasuplem4  33939  bday0s  34022  imaiinfv  40515  elrfi  40516  harval3  41145  relintab  41191  dfid7  41220  clcnvlem  41231  dfrtrcl5  41237  dfrcl2  41282  aiotajust  44576  dfaiota2  44578  ipolub0  46278
  Copyright terms: Public domain W3C validator