Theorem inteqi 4947

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

Syntax hints:   = wceq 1541  ∩ cint 4943

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-ral 3061  df-rex 3070  df-int 4944

This theorem is referenced by:  elintrab  4957  ssintrab  4968  intmin2  4972  intsng  4982  intexrab  5333  intabs  5335  op1stb  5464  dfiin3g  5956  op2ndb  6215  ordintdif  6403  knatar  7338  uniordint  7772  oawordeulem  8537  oeeulem  8584  naddov3  8662  iinfi  9394  dfttrcl2  9701  tcsni  9720  rankval2  9795  rankval3b  9803  cf0  10228  cfval2  10237  cofsmo  10246  isf34lem4  10354  isf34lem7  10356  sstskm  10819  dfnn3  12208  trclun  14943  cycsubg  19051  efgval2  19556  00lsp  20541  alexsublem  23477  noextendlt  27099  nosepne  27110  nosepdm  27114  nosupbnd2lem1  27145  noinfbnd2lem1  27160  noetasuplem4  27166  bday0s  27255  intimafv  31803  dynkin  32996  imaiinfv  41202  elrfi  41203  onuniintrab  41746  naddov4  41904  naddwordnexlem4  41923  harval3  42060  relintab  42105  dfid7  42134  clcnvlem  42145  dfrtrcl5  42151  dfrcl2  42196  aiotajust  45564  dfaiota2  45566  ipolub0  47265