Theorem inteqi 4906

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

Syntax hints:   = wceq 1541  ∩ cint 4902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-rex 3061  df-int 4903

This theorem is referenced by:  elintrab  4915  ssintrab  4926  intmin2  4930  intsng  4938  intexrab  5292  intabs  5294  op1stb  5419  dfiin3g  5918  op2ndb  6185  ordintdif  6368  knatar  7303  uniordint  7746  oawordeulem  8481  oeeulem  8529  naddov3  8608  iinfi  9320  dfttrcl2  9633  tcsni  9650  rankval2  9730  rankval3b  9738  cf0  10161  cfval2  10170  cofsmo  10179  isf34lem4  10287  isf34lem7  10289  sstskm  10753  dfnn3  12159  trclun  14937  cycsubg  19137  efgval2  19653  00lsp  20932  alexsublem  23988  noextendlt  27637  nosepne  27648  nosepdm  27652  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetasuplem4  27704  bday0  27807  intimafv  32790  dynkin  34324  rankval2b  35255  tz9.1regs  35290  imaiinfv  42931  elrfi  42932  onuniintrab  43464  naddov4  43621  naddwordnexlem4  43639  harval3  43775  relintab  43820  dfid7  43849  clcnvlem  43860  dfrtrcl5  43866  dfrcl2  43911  aiotajust  47326  dfaiota2  47328  ipolub0  49233