Theorem inteqi 4414

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

Syntax hints:   = wceq 1475  ∩ cint 4410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-int 4411

This theorem is referenced by:  elintrab  4423  ssintrab  4435  intmin2  4439  intsng  4447  intexrab  4750  intabs  4752  op1stb  4867  dfiin3g  5300  op2ndb  5537  ordintdif  5691  knatar  6507  bm2.5ii  6898  oawordeulem  7521  oeeulem  7568  iinfi  8206  tcsni  8502  rankval2  8564  rankval3b  8572  cf0  8956  cfval2  8965  cofsmo  8974  isf34lem4  9082  isf34lem7  9084  sstskm  9543  dfnn3  10911  trclun  13603  cycsubg  17445  efgval2  17960  00lsp  18802  alexsublem  21658  dynkin  29557  imaiinfv  36274  elrfi  36275  relintab  36908  dfid7  36938  clcnvlem  36949  dfrtrcl5  36955  dfrcl2  36985