Theorem inteqi 4914

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

This proof depends on syntax axioms:   = wceq 1570  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-ral 3079  df-rex 3089  df-int 4911

This theorem is used by:  elintrab  4923  ssintrab  4934  intmin2  4938  intsng  4946  intexrab  5315  intabs  5317  op1stb  5451  dfiin3g  5957  op2ndb  6227  ordintdif  6413  knatar  7364  uniordint  7804  oawordeulem  8545  oeeulem  8593  naddov3  8673  iinfi  9391  dfttrcl2  9707  tcsni  9724  rankval2  9804  rankval3b  9812  cf0  10256  cfval2  10266  cofsmo  10275  isf34lem4  10383  isf34lem7  10385  sstskm  10855  dfnn3  12275  trclun  15091  cycsubg  19342  efgval2  19857  00lsp  21171  alexsublem  24276  noextendlt  27913  nosepne  27924  nosepdm  27928  nosupbnd2lem1  27959  noinfbnd2lem1  27974  noetasuplem4  27980  bday0  28084  intimafv  33191  dynkin  34686  rankval2b  35614  tz9.1regs  35668  imaiinfv  43546  elrfi  43547  onuniintrab  44075  naddov4  44232  naddwordnexlem4  44250  harval3  44386  relintab  44431  dfid7  44460  clcnvlem  44471  dfrtrcl5  44477  dfrcl2  44522  aiotajust  47980  dfaiota2  47982  ipolub0  49926