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 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  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  7728  oawordeulem  8493  oeeulem  8540  iinfi  9311  dfttrcl2  9618  tcsni  9637  rankval2  9712  rankval3b  9720  cf0  10145  cfval2  10154  cofsmo  10163  isf34lem4  10271  isf34lem7  10273  sstskm  10736  dfnn3  12125  trclun  14859  cycsubg  18960  efgval2  19465  00lsp  20395  alexsublem  23347  noextendlt  26969  nosepne  26980  nosepdm  26984  nosupbnd2lem1  27015  noinfbnd2lem1  27030  noetasuplem4  27036  bday0s  27119  intimafv  31451  dynkin  32578  naddov3  34236  imaiinfv  40925  elrfi  40926  onuniintrab  41469  harval3  41721  relintab  41766  dfid7  41795  clcnvlem  41806  dfrtrcl5  41812  dfrcl2  41857  aiotajust  45217  dfaiota2  45219  ipolub0  46918
  Copyright terms: Public domain W3C validator