Theorem inteqi 4926

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

Syntax hints:   = wceq 1540  ∩ cint 4922

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-ral 3052  df-rex 3061  df-int 4923

This theorem is referenced by:  elintrab  4936  ssintrab  4947  intmin2  4951  intsng  4959  intexrab  5317  intabs  5319  op1stb  5446  dfiin3g  5948  op2ndb  6216  ordintdif  6403  knatar  7350  uniordint  7795  oawordeulem  8566  oeeulem  8613  naddov3  8692  iinfi  9429  dfttrcl2  9738  tcsni  9757  rankval2  9832  rankval3b  9840  cf0  10265  cfval2  10274  cofsmo  10283  isf34lem4  10391  isf34lem7  10393  sstskm  10856  dfnn3  12254  trclun  15033  cycsubg  19191  efgval2  19705  00lsp  20938  alexsublem  23982  noextendlt  27633  nosepne  27644  nosepdm  27648  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetasuplem4  27700  bday0s  27792  intimafv  32688  dynkin  34198  imaiinfv  42716  elrfi  42717  onuniintrab  43250  naddov4  43407  naddwordnexlem4  43425  harval3  43562  relintab  43607  dfid7  43636  clcnvlem  43647  dfrtrcl5  43653  dfrcl2  43698  aiotajust  47113  dfaiota2  47115  ipolub0  48966