Theorem inteqi 4901

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

Syntax hints:   = wceq 1541  ∩ cint 4897

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-ral 3049  df-rex 3058  df-int 4898

This theorem is referenced by:  elintrab  4910  ssintrab  4921  intmin2  4925  intsng  4933  intexrab  5287  intabs  5289  op1stb  5414  dfiin3g  5912  op2ndb  6179  ordintdif  6362  knatar  7297  uniordint  7740  oawordeulem  8475  oeeulem  8522  naddov3  8601  iinfi  9308  dfttrcl2  9621  tcsni  9638  rankval2  9718  rankval3b  9726  cf0  10149  cfval2  10158  cofsmo  10167  isf34lem4  10275  isf34lem7  10277  sstskm  10740  dfnn3  12146  trclun  14923  cycsubg  19122  efgval2  19638  00lsp  20916  alexsublem  23960  noextendlt  27609  nosepne  27620  nosepdm  27624  nosupbnd2lem1  27655  noinfbnd2lem1  27670  noetasuplem4  27676  bday0s  27773  intimafv  32696  dynkin  34201  rankval2b  35131  tz9.1regs  35151  imaiinfv  42810  elrfi  42811  onuniintrab  43343  naddov4  43500  naddwordnexlem4  43518  harval3  43655  relintab  43700  dfid7  43729  clcnvlem  43740  dfrtrcl5  43746  dfrcl2  43791  aiotajust  47208  dfaiota2  47210  ipolub0  49116