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

Theorem inteqi 4449
 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 4448 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
 Colors of variables: wff setvar class Syntax hints:   = wceq 1480  ∩ cint 4445 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-int 4446 This theorem is referenced by:  elintrab  4458  ssintrab  4470  intmin2  4474  intsng  4482  intexrab  4788  intabs  4790  op1stb  4906  dfiin3g  5344  op2ndb  5583  ordintdif  5738  knatar  6567  bm2.5ii  6960  oawordeulem  7586  oeeulem  7633  iinfi  8275  tcsni  8571  rankval2  8633  rankval3b  8641  cf0  9025  cfval2  9034  cofsmo  9043  isf34lem4  9151  isf34lem7  9153  sstskm  9616  dfnn3  10986  trclun  13697  cycsubg  17554  efgval2  18069  00lsp  18913  alexsublem  21771  dynkin  30035  noextendlt  31561  nosepne  31601  nosepdm  31603  imaiinfv  36771  elrfi  36772  relintab  37405  dfid7  37435  clcnvlem  37446  dfrtrcl5  37452  dfrcl2  37482
 Copyright terms: Public domain W3C validator