Theorem inteqi 4954

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

Syntax hints:   = wceq 1536  ∩ cint 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-ral 3059  df-rex 3068  df-int 4951

This theorem is referenced by:  elintrab  4964  ssintrab  4975  intmin2  4979  intsng  4987  intexrab  5352  intabs  5354  op1stb  5481  dfiin3g  5981  op2ndb  6248  ordintdif  6435  knatar  7376  uniordint  7820  oawordeulem  8590  oeeulem  8637  naddov3  8716  iinfi  9454  dfttrcl2  9761  tcsni  9780  rankval2  9855  rankval3b  9863  cf0  10288  cfval2  10297  cofsmo  10306  isf34lem4  10414  isf34lem7  10416  sstskm  10879  dfnn3  12277  trclun  15049  cycsubg  19238  efgval2  19756  00lsp  20996  alexsublem  24067  noextendlt  27728  nosepne  27739  nosepdm  27743  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetasuplem4  27795  bday0s  27887  intimafv  32725  dynkin  34147  imaiinfv  42680  elrfi  42681  onuniintrab  43214  naddov4  43372  naddwordnexlem4  43390  harval3  43527  relintab  43572  dfid7  43601  clcnvlem  43612  dfrtrcl5  43618  dfrcl2  43663  aiotajust  47033  dfaiota2  47035  ipolub0  48780