Theorem inteqi 4912

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

Syntax hints:   = wceq 1563  ∩ cint 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ral 3080  df-rex 3090  df-int 4909

This theorem is referenced by:  elintrab  4921  ssintrab  4932  intmin2  4936  intsng  4944  intexrab  5308  intabs  5310  op1stb  5444  dfiin3g  5950  op2ndb  6218  ordintdif  6401  knatar  7345  uniordint  7788  oawordeulem  8527  oeeulem  8575  naddov3  8655  iinfi  9365  dfttrcl2  9681  tcsni  9698  rankval2  9778  rankval3b  9786  cf0  10222  cfval2  10232  cofsmo  10241  isf34lem4  10349  isf34lem7  10351  sstskm  10815  dfnn3  12238  trclun  15041  cycsubg  19270  efgval2  19785  00lsp  21071  alexsublem  24162  noextendlt  27791  nosepne  27802  nosepdm  27806  nosupbnd2lem1  27837  noinfbnd2lem1  27852  noetasuplem4  27858  bday0  27962  intimafv  32968  dynkin  34474  rankval2b  35407  tz9.1regs  35442  imaiinfv  43286  elrfi  43287  onuniintrab  43815  naddov4  43972  naddwordnexlem4  43990  harval3  44126  relintab  44171  dfid7  44200  clcnvlem  44211  dfrtrcl5  44217  dfrcl2  44262  aiotajust  47676  dfaiota2  47678  ipolub0  49621