Theorem inteqi 4950

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

Syntax hints:   = wceq 1540  ∩ cint 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ral 3062  df-rex 3071  df-int 4947

This theorem is referenced by:  elintrab  4960  ssintrab  4971  intmin2  4975  intsng  4983  intexrab  5347  intabs  5349  op1stb  5476  dfiin3g  5979  op2ndb  6247  ordintdif  6434  knatar  7377  uniordint  7821  oawordeulem  8592  oeeulem  8639  naddov3  8718  iinfi  9457  dfttrcl2  9764  tcsni  9783  rankval2  9858  rankval3b  9866  cf0  10291  cfval2  10300  cofsmo  10309  isf34lem4  10417  isf34lem7  10419  sstskm  10882  dfnn3  12280  trclun  15053  cycsubg  19226  efgval2  19742  00lsp  20979  alexsublem  24052  noextendlt  27714  nosepne  27725  nosepdm  27729  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  bday0s  27873  intimafv  32720  dynkin  34168  imaiinfv  42704  elrfi  42705  onuniintrab  43238  naddov4  43396  naddwordnexlem4  43414  harval3  43551  relintab  43596  dfid7  43625  clcnvlem  43636  dfrtrcl5  43642  dfrcl2  43687  aiotajust  47096  dfaiota2  47098  ipolub0  48881