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

Step	Hyp	Ref	Expression
1		inteqi.1	. 2
2		inteq 4289	. 2
3	1, 2	ax-mp 5	1

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