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 ⊢ ∩ 𝐴 = ∩ 𝐵

Syntax hints:   = wceq 1540  ∩ cint 4910

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-rex 3054  df-int 4911

This theorem is referenced by:  elintrab  4924  ssintrab  4935  intmin2  4939  intsng  4947  intexrab  5302  intabs  5304  op1stb  5431  dfiin3g  5932  op2ndb  6200  ordintdif  6383  knatar  7332  uniordint  7777  oawordeulem  8518  oeeulem  8565  naddov3  8644  iinfi  9368  dfttrcl2  9677  tcsni  9696  rankval2  9771  rankval3b  9779  cf0  10204  cfval2  10213  cofsmo  10222  isf34lem4  10330  isf34lem7  10332  sstskm  10795  dfnn3  12200  trclun  14980  cycsubg  19140  efgval2  19654  00lsp  20887  alexsublem  23931  noextendlt  27581  nosepne  27592  nosepdm  27596  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem4  27648  bday0s  27740  intimafv  32634  dynkin  34157  imaiinfv  42681  elrfi  42682  onuniintrab  43215  naddov4  43372  naddwordnexlem4  43390  harval3  43527  relintab  43572  dfid7  43601  clcnvlem  43612  dfrtrcl5  43618  dfrcl2  43663  aiotajust  47085  dfaiota2  47087  ipolub0  48980