Theorem inteqi 4908

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

Syntax hints:   = wceq 1542  ∩ cint 4904

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rex 3063  df-int 4905

This theorem is referenced by:  elintrab  4917  ssintrab  4928  intmin2  4932  intsng  4940  intexrab  5294  intabs  5296  op1stb  5427  dfiin3g  5926  op2ndb  6193  ordintdif  6376  knatar  7313  uniordint  7756  oawordeulem  8491  oeeulem  8539  naddov3  8618  iinfi  9332  dfttrcl2  9645  tcsni  9662  rankval2  9742  rankval3b  9750  cf0  10173  cfval2  10182  cofsmo  10191  isf34lem4  10299  isf34lem7  10301  sstskm  10765  dfnn3  12171  trclun  14949  cycsubg  19149  efgval2  19665  00lsp  20944  alexsublem  24000  noextendlt  27649  nosepne  27660  nosepdm  27664  nosupbnd2lem1  27695  noinfbnd2lem1  27710  noetasuplem4  27716  bday0  27819  intimafv  32800  dynkin  34344  rankval2b  35274  tz9.1regs  35309  imaiinfv  43044  elrfi  43045  onuniintrab  43577  naddov4  43734  naddwordnexlem4  43752  harval3  43888  relintab  43933  dfid7  43962  clcnvlem  43973  dfrtrcl5  43979  dfrcl2  44024  aiotajust  47438  dfaiota2  47440  ipolub0  49345