Theorem inteqi 4954

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

Syntax hints:   = wceq 1541  ∩ cint 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-ral 3062  df-rex 3071  df-int 4951

This theorem is referenced by:  elintrab  4964  ssintrab  4975  intmin2  4979  intsng  4989  intexrab  5340  intabs  5342  op1stb  5471  dfiin3g  5964  op2ndb  6226  ordintdif  6414  knatar  7356  uniordint  7791  oawordeulem  8556  oeeulem  8603  naddov3  8681  iinfi  9414  dfttrcl2  9721  tcsni  9740  rankval2  9815  rankval3b  9823  cf0  10248  cfval2  10257  cofsmo  10266  isf34lem4  10374  isf34lem7  10376  sstskm  10839  dfnn3  12230  trclun  14965  cycsubg  19123  efgval2  19633  00lsp  20736  alexsublem  23768  noextendlt  27396  nosepne  27407  nosepdm  27411  nosupbnd2lem1  27442  noinfbnd2lem1  27457  noetasuplem4  27463  bday0s  27554  intimafv  32187  dynkin  33451  imaiinfv  41733  elrfi  41734  onuniintrab  42277  naddov4  42435  naddwordnexlem4  42454  harval3  42591  relintab  42636  dfid7  42665  clcnvlem  42676  dfrtrcl5  42682  dfrcl2  42727  aiotajust  46091  dfaiota2  46093  ipolub0  47705