Theorem inteqi 4714

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

Syntax hints:   = wceq 1601  ∩ cint 4710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1605  df-ex 1824  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-ral 3094  df-int 4711

This theorem is referenced by:  elintrab  4722  ssintrab  4733  intmin2  4737  intsng  4745  intexrab  5057  intabs  5059  op1stb  5171  dfiin3g  5625  op2ndb  5874  ordintdif  6025  knatar  6879  uniordint  7284  oawordeulem  7918  oeeulem  7965  iinfi  8611  tcsni  8916  rankval2  8978  rankval3b  8986  cf0  9408  cfval2  9417  cofsmo  9426  isf34lem4  9534  isf34lem7  9536  sstskm  9999  dfnn3  11390  trclun  14162  cycsubg  18006  efgval2  18521  00lsp  19376  alexsublem  22256  dynkin  30842  noextendlt  32425  nosepne  32434  nosepdm  32437  nosupbnd2lem1  32464  noetalem3  32468  imaiinfv  38208  elrfi  38209  relintab  38838  dfid7  38868  clcnvlem  38879  dfrtrcl5  38885  dfrcl2  38915  aiotajust  42106  dfaiota2  42108