Theorem inteqi 4955

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

Syntax hints:   = wceq 1542  ∩ cint 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ral 3063  df-rex 3072  df-int 4952

This theorem is referenced by:  elintrab  4965  ssintrab  4976  intmin2  4980  intsng  4990  intexrab  5341  intabs  5343  op1stb  5472  dfiin3g  5965  op2ndb  6227  ordintdif  6415  knatar  7354  uniordint  7789  oawordeulem  8554  oeeulem  8601  naddov3  8679  iinfi  9412  dfttrcl2  9719  tcsni  9738  rankval2  9813  rankval3b  9821  cf0  10246  cfval2  10255  cofsmo  10264  isf34lem4  10372  isf34lem7  10374  sstskm  10837  dfnn3  12226  trclun  14961  cycsubg  19085  efgval2  19592  00lsp  20592  alexsublem  23548  noextendlt  27172  nosepne  27183  nosepdm  27187  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetasuplem4  27239  bday0s  27329  intimafv  31932  dynkin  33165  imaiinfv  41431  elrfi  41432  onuniintrab  41975  naddov4  42133  naddwordnexlem4  42152  harval3  42289  relintab  42334  dfid7  42363  clcnvlem  42374  dfrtrcl5  42380  dfrcl2  42425  aiotajust  45792  dfaiota2  45794  ipolub0  47617