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

Theorem inteqi 4511
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 4510 . 2 (𝐴 = 𝐵 𝐴 = 𝐵)
31, 2ax-mp 5 1 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523   cint 4507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-int 4508
This theorem is referenced by:  elintrab  4520  ssintrab  4532  intmin2  4536  intsng  4544  intexrab  4853  intabs  4855  op1stb  4969  dfiin3g  5411  op2ndb  5657  ordintdif  5812  knatar  6647  bm2.5ii  7048  oawordeulem  7679  oeeulem  7726  iinfi  8364  tcsni  8657  rankval2  8719  rankval3b  8727  cf0  9111  cfval2  9120  cofsmo  9129  isf34lem4  9237  isf34lem7  9239  sstskm  9702  dfnn3  11072  trclun  13799  cycsubg  17669  efgval2  18183  00lsp  19029  alexsublem  21895  dynkin  30358  noextendlt  31947  nosepne  31956  nosepdm  31959  nosupbnd2lem1  31986  noetalem3  31990  imaiinfv  37573  elrfi  37574  relintab  38206  dfid7  38236  clcnvlem  38247  dfrtrcl5  38253  dfrcl2  38283
  Copyright terms: Public domain W3C validator