Theorem inteqi 4910

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

This proof depends on syntax axioms:   = wceq 1569  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-rex 3087  df-int 4907

This theorem is used by:  elintrab  4919  ssintrab  4930  intmin2  4934  intsng  4942  intexrab  5307  intabs  5309  op1stb  5439  dfiin3g  5950  op2ndb  6228  ordintdif  6414  knatar  7367  uniordint  7815  oawordeulem  8565  oeeulem  8613  naddov3  8693  iinfi  9412  dfttrcl2  9728  tcsni  9745  rankval2  9830  rankval2b  9838  rankval3b  9839  cf0  10331  cfval2  10341  cofsmo  10350  isf34lem4  10458  isf34lem7  10460  sstskm  10930  dfnn3  12352  trclun  15172  cycsubg  19428  efgval2  19943  00lsp  21261  alexsublem  24368  noextendlt  28031  nosepne  28042  nosepdm  28046  nosupbnd2lem1  28077  noinfbnd2lem1  28092  noetasuplem4  28098  bday0  28202  intimafv  33351  dynkin  34846  tz9.1regs  35858  imaiinfv  43797  elrfi  43798  onuniintrab  44321  naddov4  44478  naddwordnexlem4  44496  harval3  44632  relintab  44677  dfid7  44705  clcnvlem  44716  dfrtrcl5  44722  dfrcl2  44767  aiotajust  48247  dfaiota2  48249  ipolub0  50199