Theorem inteqi 4917

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

Syntax hints:   = wceq 1540  ∩ cint 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-ral 3046  df-rex 3055  df-int 4914

This theorem is referenced by:  elintrab  4927  ssintrab  4938  intmin2  4942  intsng  4950  intexrab  5305  intabs  5307  op1stb  5434  dfiin3g  5935  op2ndb  6203  ordintdif  6386  knatar  7335  uniordint  7780  oawordeulem  8521  oeeulem  8568  naddov3  8647  iinfi  9375  dfttrcl2  9684  tcsni  9703  rankval2  9778  rankval3b  9786  cf0  10211  cfval2  10220  cofsmo  10229  isf34lem4  10337  isf34lem7  10339  sstskm  10802  dfnn3  12207  trclun  14987  cycsubg  19147  efgval2  19661  00lsp  20894  alexsublem  23938  noextendlt  27588  nosepne  27599  nosepdm  27603  nosupbnd2lem1  27634  noinfbnd2lem1  27649  noetasuplem4  27655  bday0s  27747  intimafv  32641  dynkin  34164  imaiinfv  42688  elrfi  42689  onuniintrab  43222  naddov4  43379  naddwordnexlem4  43397  harval3  43534  relintab  43579  dfid7  43608  clcnvlem  43619  dfrtrcl5  43625  dfrcl2  43670  aiotajust  47089  dfaiota2  47091  ipolub0  48984