Theorem inteqi 4911

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 4910	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ∩ 𝐴 = ∩ 𝐵

This proof depends on syntax axioms:   = wceq 1570  ∩ cint 4907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-ral 3078  df-rex 3088  df-int 4908

This theorem is used by:  elintrab  4920  ssintrab  4931  intmin2  4935  intsng  4943  intexrab  5308  intabs  5310  op1stb  5440  dfiin3g  5951  op2ndb  6221  ordintdif  6407  knatar  7359  uniordint  7804  oawordeulem  8546  oeeulem  8594  naddov3  8674  iinfi  9393  dfttrcl2  9709  tcsni  9726  rankval2  9808  rankval2b  9816  rankval3b  9817  cf0  10309  cfval2  10319  cofsmo  10328  isf34lem4  10436  isf34lem7  10438  sstskm  10908  dfnn3  12330  trclun  15147  cycsubg  19403  efgval2  19918  00lsp  21236  alexsublem  24343  noextendlt  28008  nosepne  28019  nosepdm  28023  nosupbnd2lem1  28054  noinfbnd2lem1  28069  noetasuplem4  28075  bday0  28179  intimafv  33286  dynkin  34782  tz9.1regs  35775  imaiinfv  43657  elrfi  43658  onuniintrab  44186  naddov4  44343  naddwordnexlem4  44361  harval3  44497  relintab  44542  dfid7  44571  clcnvlem  44582  dfrtrcl5  44588  dfrcl2  44633  aiotajust  48098  dfaiota2  48100  ipolub0  50044