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

Theorem inteqi 4889
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 4888 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   cint 4885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-ral 3071  df-int 4886
This theorem is referenced by:  elintrab  4897  ssintrab  4908  intmin2  4912  intsng  4922  intexrab  5268  intabs  5270  op1stb  5390  dfiin3g  5873  op2ndb  6129  ordintdif  6314  knatar  7225  uniordint  7646  oawordeulem  8377  oeeulem  8424  iinfi  9164  dfttrcl2  9470  tcsni  9511  rankval2  9587  rankval3b  9595  cf0  10018  cfval2  10027  cofsmo  10036  isf34lem4  10144  isf34lem7  10146  sstskm  10609  dfnn3  11998  trclun  14736  cycsubg  18838  efgval2  19341  00lsp  20254  alexsublem  23206  intimafv  31052  dynkin  32144  noextendlt  33881  nosepne  33892  nosepdm  33896  nosupbnd2lem1  33927  noinfbnd2lem1  33942  noetasuplem4  33948  bday0s  34031  imaiinfv  40524  elrfi  40525  harval3  41134  relintab  41173  dfid7  41202  clcnvlem  41213  dfrtrcl5  41219  dfrcl2  41264  aiotajust  44555  dfaiota2  44557  ipolub0  46257
  Copyright terms: Public domain W3C validator