Theorem inteqi 4893

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

Syntax hints:   = wceq 1542  ∩ cint 4889

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ral 3052  df-rex 3062  df-int 4890

This theorem is referenced by:  elintrab  4902  ssintrab  4913  intmin2  4917  intsng  4925  intexrab  5288  intabs  5290  op1stb  5424  dfiin3g  5924  op2ndb  6191  ordintdif  6374  knatar  7312  uniordint  7755  oawordeulem  8489  oeeulem  8537  naddov3  8616  iinfi  9330  dfttrcl2  9645  tcsni  9662  rankval2  9742  rankval3b  9750  cf0  10173  cfval2  10182  cofsmo  10191  isf34lem4  10299  isf34lem7  10301  sstskm  10765  dfnn3  12188  trclun  14976  cycsubg  19183  efgval2  19699  00lsp  20976  alexsublem  24009  noextendlt  27633  nosepne  27644  nosepdm  27648  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  bday0  27803  intimafv  32784  dynkin  34311  rankval2b  35242  tz9.1regs  35278  imaiinfv  43125  elrfi  43126  onuniintrab  43654  naddov4  43811  naddwordnexlem4  43829  harval3  43965  relintab  44010  dfid7  44039  clcnvlem  44050  dfrtrcl5  44056  dfrcl2  44101  aiotajust  47532  dfaiota2  47534  ipolub0  49467