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 1559  ∩ cint 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-ral 3076  df-rex 3086  df-int 4905

This theorem is referenced by:  elintrab  4917  ssintrab  4928  intmin2  4932  intsng  4940  intexrab  5302  intabs  5304  op1stb  5438  dfiin3g  5943  op2ndb  6210  ordintdif  6393  knatar  7337  uniordint  7780  oawordeulem  8518  oeeulem  8566  naddov3  8646  iinfi  9360  dfttrcl2  9676  tcsni  9693  rankval2  9773  rankval3b  9781  cf0  10204  cfval2  10214  cofsmo  10223  isf34lem4  10331  isf34lem7  10333  sstskm  10797  dfnn3  12221  trclun  15024  cycsubg  19232  efgval2  19747  00lsp  21028  alexsublem  24084  noextendlt  27710  nosepne  27721  nosepdm  27725  nosupbnd2lem1  27756  noinfbnd2lem1  27771  noetasuplem4  27777  bday0  27881  intimafv  32863  dynkin  34425  rankval2b  35359  tz9.1regs  35394  imaiinfv  43238  elrfi  43239  onuniintrab  43767  naddov4  43924  naddwordnexlem4  43942  harval3  44078  relintab  44123  dfid7  44152  clcnvlem  44163  dfrtrcl5  44169  dfrcl2  44214  aiotajust  47642  dfaiota2  47644  ipolub0  49577