Theorem inteqi 4914

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-rex 3091  df-int 4911

This theorem is used by:  elintrab  4923  ssintrab  4934  intmin2  4938  intsng  4946  intexrab  5312  intabs  5314  op1stb  5444  dfiin3g  5958  op2ndb  6241  ordintdif  6432  knatar  7390  uniordint  7839  oawordeulem  8590  oeeulem  8638  naddov3  8718  iinfi  9436  dfttrcl2  9752  tcsni  9769  rankval2  9854  rankval2b  9862  rankval3b  9863  cf0  10355  cfval2  10365  cofsmo  10374  isf34lem4  10482  isf34lem7  10484  sstskm  10954  dfnn3  12376  trclun  15196  cycsubg  19452  efgval2  19968  00lsp  21286  alexsublem  24393  noextendlt  28056  nosepne  28067  nosepdm  28071  nosupbnd2lem1  28102  noinfbnd2lem1  28117  noetasuplem4  28123  bday0  28227  intimafv  33375  dynkin  34870  tz9.1regs  35902  imaiinfv  43897  elrfi  43898  onuniintrab  44420  naddov4  44577  naddwordnexlem4  44595  harval3  44731  relintab  44776  dfid7  44804  clcnvlem  44815  dfrtrcl5  44821  dfrcl2  44866  aiotajust  48359  dfaiota2  48361  ipolub0  50311