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

Theorem inteqi 4909
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 4908 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541   cint 4905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-ral 3063  df-int 4906
This theorem is referenced by:  elintrab  4919  ssintrab  4930  intmin2  4934  intsng  4944  intexrab  5295  intabs  5297  op1stb  5426  dfiin3g  5918  op2ndb  6177  ordintdif  6365  knatar  7298  uniordint  7732  oawordeulem  8497  oeeulem  8544  naddov3  8622  iinfi  9349  dfttrcl2  9656  tcsni  9675  rankval2  9750  rankval3b  9758  cf0  10183  cfval2  10192  cofsmo  10201  isf34lem4  10309  isf34lem7  10311  sstskm  10774  dfnn3  12163  trclun  14891  cycsubg  18992  efgval2  19497  00lsp  20427  alexsublem  23379  noextendlt  27001  nosepne  27012  nosepdm  27016  nosupbnd2lem1  27047  noinfbnd2lem1  27062  noetasuplem4  27068  bday0s  27151  intimafv  31508  dynkin  32635  imaiinfv  40954  elrfi  40955  onuniintrab  41498  harval3  41752  relintab  41797  dfid7  41826  clcnvlem  41837  dfrtrcl5  41843  dfrcl2  41888  aiotajust  45248  dfaiota2  45250  ipolub0  46949
  Copyright terms: Public domain W3C validator