Theorem inteqi 4917

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

Syntax hints:   = wceq 1570  ∩ cint 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-rex 3090  df-int 4914

This theorem is referenced by:  elintrab  4926  ssintrab  4937  intmin2  4941  intsng  4949  intexrab  5319  intabs  5321  op1stb  5455  dfiin3g  5961  op2ndb  6230  ordintdif  6414  knatar  7357  uniordint  7801  oawordeulem  8540  oeeulem  8588  naddov3  8668  iinfi  9378  dfttrcl2  9694  tcsni  9711  rankval2  9791  rankval3b  9799  cf0  10235  cfval2  10245  cofsmo  10254  isf34lem4  10362  isf34lem7  10364  sstskm  10828  dfnn3  12248  trclun  15053  cycsubg  19280  efgval2  19795  00lsp  21083  alexsublem  24182  noextendlt  27811  nosepne  27822  nosepdm  27826  nosupbnd2lem1  27857  noinfbnd2lem1  27872  noetasuplem4  27878  bday0  27982  intimafv  33034  dynkin  34535  rankval2b  35470  tz9.1regs  35525  imaiinfv  43404  elrfi  43405  onuniintrab  43933  naddov4  44090  naddwordnexlem4  44108  harval3  44244  relintab  44289  dfid7  44318  clcnvlem  44329  dfrtrcl5  44335  dfrcl2  44380  aiotajust  47798  dfaiota2  47800  ipolub0  49747