Theorem inteqi 4894

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

Syntax hints:   = wceq 1542  ∩ cint 4890

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rex 3063  df-int 4891

This theorem is referenced by:  elintrab  4903  ssintrab  4914  intmin2  4918  intsng  4926  intexrab  5284  intabs  5286  op1stb  5419  dfiin3g  5918  op2ndb  6185  ordintdif  6368  knatar  7305  uniordint  7748  oawordeulem  8482  oeeulem  8530  naddov3  8609  iinfi  9323  dfttrcl2  9636  tcsni  9653  rankval2  9733  rankval3b  9741  cf0  10164  cfval2  10173  cofsmo  10182  isf34lem4  10290  isf34lem7  10292  sstskm  10756  dfnn3  12179  trclun  14967  cycsubg  19174  efgval2  19690  00lsp  20967  alexsublem  24019  noextendlt  27647  nosepne  27658  nosepdm  27662  nosupbnd2lem1  27693  noinfbnd2lem1  27708  noetasuplem4  27714  bday0  27817  intimafv  32799  dynkin  34327  rankval2b  35258  tz9.1regs  35294  imaiinfv  43139  elrfi  43140  onuniintrab  43672  naddov4  43829  naddwordnexlem4  43847  harval3  43983  relintab  44028  dfid7  44057  clcnvlem  44068  dfrtrcl5  44074  dfrcl2  44119  aiotajust  47544  dfaiota2  47546  ipolub0  49479