Theorem inteqi 4921

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

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

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 4918

This theorem is used by:  elintrab  4930  ssintrab  4941  intmin2  4945  intsng  4953  intexrab  5322  intabs  5324  op1stb  5458  dfiin3g  5964  op2ndb  6233  ordintdif  6419  knatar  7368  uniordint  7809  oawordeulem  8548  oeeulem  8596  naddov3  8676  iinfi  9387  dfttrcl2  9703  tcsni  9720  rankval2  9800  rankval3b  9808  cf0  10252  cfval2  10262  cofsmo  10271  isf34lem4  10379  isf34lem7  10381  sstskm  10845  dfnn3  12265  trclun  15077  cycsubg  19310  efgval2  19825  00lsp  21139  alexsublem  24238  noextendlt  27870  nosepne  27881  nosepdm  27885  nosupbnd2lem1  27916  noinfbnd2lem1  27931  noetasuplem4  27937  bday0  28041  intimafv  33093  dynkin  34589  rankval2b  35517  tz9.1regs  35571  imaiinfv  43465  elrfi  43466  onuniintrab  43994  naddov4  44151  naddwordnexlem4  44169  harval3  44305  relintab  44350  dfid7  44379  clcnvlem  44390  dfrtrcl5  44396  dfrcl2  44441  aiotajust  47862  dfaiota2  47864  ipolub0  49811