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

Theorem inteqi 4882
 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 4881 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
 Colors of variables: wff setvar class Syntax hints:   = wceq 1537  ∩ cint 4878 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-int 4879 This theorem is referenced by:  elintrab  4890  ssintrab  4901  intmin2  4905  intsng  4913  intexrab  5245  intabs  5247  op1stb  5365  dfiin3g  5838  op2ndb  6086  ordintdif  6242  knatar  7112  uniordint  7523  oawordeulem  8182  oeeulem  8229  iinfi  8883  tcsni  9187  rankval2  9249  rankval3b  9257  cf0  9675  cfval2  9684  cofsmo  9693  isf34lem4  9801  isf34lem7  9803  sstskm  10266  dfnn3  11654  trclun  14376  cycsubg  18353  efgval2  18852  00lsp  19755  alexsublem  22654  dynkin  31428  noextendlt  33178  nosepne  33187  nosepdm  33190  nosupbnd2lem1  33217  noetalem3  33221  imaiinfv  39297  elrfi  39298  harval3  39911  relintab  39950  dfid7  39979  clcnvlem  39990  dfrtrcl5  39996  dfrcl2  40026  aiotajust  43291  dfaiota2  43293
 Copyright terms: Public domain W3C validator