Theorem inteqi 4882

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

Syntax hints:   = wceq 1537  ∩ cint 4878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-int 4879

This theorem is referenced by:  elintrab  4890  ssintrab  4901  intmin2  4905  intsng  4913  intexrab  5245  intabs  5247  op1stb  5365  dfiin3g  5838  op2ndb  6086  ordintdif  6242  knatar  7112  uniordint  7523  oawordeulem  8182  oeeulem  8229  iinfi  8883  tcsni  9187  rankval2  9249  rankval3b  9257  cf0  9675  cfval2  9684  cofsmo  9693  isf34lem4  9801  isf34lem7  9803  sstskm  10266  dfnn3  11654  trclun  14376  cycsubg  18353  efgval2  18852  00lsp  19755  alexsublem  22654  dynkin  31428  noextendlt  33178  nosepne  33187  nosepdm  33190  nosupbnd2lem1  33217  noetalem3  33221  imaiinfv  39297  elrfi  39298  harval3  39911  relintab  39950  dfid7  39979  clcnvlem  39990  dfrtrcl5  39996  dfrcl2  40026  aiotajust  43291  dfaiota2  43293