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

Theorem inteqi 4290
 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 4289 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  |^|cint 4286 This theorem is referenced by:  elintrab  4298  ssintrab  4310  intmin2  4314  intsng  4322  intexrab  4611  intabs  4613  op1stb  4722  ordintdif  4932  dfiin3g  5261  op2ndb  5497  knatar  6253  bm2.5ii  6641  oawordeulem  7222  oeeulem  7269  iinfi  7897  tcsni  8195  rankval2  8257  rankval3b  8265  cf0  8652  cfval2  8661  cofsmo  8670  isf34lem4  8778  isf34lem7  8780  sstskm  9241  dfnn3  10575  cycsubg  16229  efgval2  16742  00lsp  17627  alexsublem  20544  imaiinfv  30625  elrfi  30626 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-int 4287
 Copyright terms: Public domain W3C validator