Theorem inteqi 4901

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

Syntax hints:   = wceq 1541  ∩ cint 4897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ral 3048  df-rex 3057  df-int 4898

This theorem is referenced by:  elintrab  4910  ssintrab  4921  intmin2  4925  intsng  4933  intexrab  5285  intabs  5287  op1stb  5411  dfiin3g  5908  op2ndb  6174  ordintdif  6357  knatar  7291  uniordint  7734  oawordeulem  8469  oeeulem  8516  naddov3  8595  iinfi  9301  dfttrcl2  9614  tcsni  9633  rankval2  9708  rankval3b  9716  cf0  10139  cfval2  10148  cofsmo  10157  isf34lem4  10265  isf34lem7  10267  sstskm  10730  dfnn3  12136  trclun  14918  cycsubg  19118  efgval2  19634  00lsp  20912  alexsublem  23957  noextendlt  27606  nosepne  27617  nosepdm  27621  nosupbnd2lem1  27652  noinfbnd2lem1  27667  noetasuplem4  27673  bday0s  27770  intimafv  32687  dynkin  34175  rankval2b  35103  tz9.1regs  35118  imaiinfv  42725  elrfi  42726  onuniintrab  43258  naddov4  43415  naddwordnexlem4  43433  harval3  43570  relintab  43615  dfid7  43644  clcnvlem  43655  dfrtrcl5  43661  dfrcl2  43706  aiotajust  47114  dfaiota2  47116  ipolub0  49022