Theorem inteqi 4919

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

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

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-ral 3083  df-rex 3093  df-int 4916

This theorem is used by:  elintrab  4928  ssintrab  4939  intmin2  4943  intsng  4951  intexrab  5320  intabs  5322  op1stb  5456  dfiin3g  5962  op2ndb  6231  ordintdif  6416  knatar  7361  uniordint  7802  oawordeulem  8541  oeeulem  8589  naddov3  8669  iinfi  9379  dfttrcl2  9695  tcsni  9712  rankval2  9792  rankval3b  9800  cf0  10244  cfval2  10254  cofsmo  10263  isf34lem4  10371  isf34lem7  10373  sstskm  10837  dfnn3  12257  trclun  15062  cycsubg  19289  efgval2  19804  00lsp  21117  alexsublem  24216  noextendlt  27848  nosepne  27859  nosepdm  27863  nosupbnd2lem1  27894  noinfbnd2lem1  27909  noetasuplem4  27915  bday0  28019  intimafv  33071  dynkin  34570  rankval2b  35505  tz9.1regs  35559  imaiinfv  43456  elrfi  43457  onuniintrab  43985  naddov4  44142  naddwordnexlem4  44160  harval3  44296  relintab  44341  dfid7  44370  clcnvlem  44381  dfrtrcl5  44387  dfrcl2  44432  aiotajust  47853  dfaiota2  47855  ipolub0  49802