Theorem inteqi 4880

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

Syntax hints:   = wceq 1539  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-ral 3068  df-int 4877

This theorem is referenced by:  elintrab  4888  ssintrab  4899  intmin2  4903  intsng  4913  intexrab  5259  intabs  5261  op1stb  5380  dfiin3g  5863  op2ndb  6119  ordintdif  6300  knatar  7208  uniordint  7628  oawordeulem  8347  oeeulem  8394  iinfi  9106  tcsni  9432  rankval2  9507  rankval3b  9515  cf0  9938  cfval2  9947  cofsmo  9956  isf34lem4  10064  isf34lem7  10066  sstskm  10529  dfnn3  11917  trclun  14653  cycsubg  18742  efgval2  19245  00lsp  20158  alexsublem  23103  intimafv  30945  dynkin  32035  dfttrcl2  33710  noextendlt  33799  nosepne  33810  nosepdm  33814  nosupbnd2lem1  33845  noinfbnd2lem1  33860  noetasuplem4  33866  bday0s  33949  imaiinfv  40431  elrfi  40432  harval3  41041  relintab  41080  dfid7  41109  clcnvlem  41120  dfrtrcl5  41126  dfrcl2  41171  aiotajust  44463  dfaiota2  44465  ipolub0  46166