Theorem inteqi 4842

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

Syntax hints:   = wceq 1538  ∩ cint 4838

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-int 4839

This theorem is referenced by:  elintrab  4850  ssintrab  4861  intmin2  4865  intsng  4873  intexrab  5207  intabs  5209  op1stb  5328  dfiin3g  5801  op2ndb  6051  ordintdif  6208  knatar  7089  uniordint  7501  oawordeulem  8163  oeeulem  8210  iinfi  8865  tcsni  9169  rankval2  9231  rankval3b  9239  cf0  9662  cfval2  9671  cofsmo  9680  isf34lem4  9788  isf34lem7  9790  sstskm  10253  dfnn3  11639  trclun  14365  cycsubg  18343  efgval2  18842  00lsp  19746  alexsublem  22649  intimafv  30470  dynkin  31536  noextendlt  33289  nosepne  33298  nosepdm  33301  nosupbnd2lem1  33328  noetalem3  33332  imaiinfv  39634  elrfi  39635  harval3  40244  relintab  40283  dfid7  40312  clcnvlem  40323  dfrtrcl5  40329  dfrcl2  40375  aiotajust  43641  dfaiota2  43643