Theorem inteqi 4974

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

Syntax hints:   = wceq 1537  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ral 3068  df-rex 3077  df-int 4971

This theorem is referenced by:  elintrab  4984  ssintrab  4995  intmin2  4999  intsng  5007  intexrab  5365  intabs  5367  op1stb  5491  dfiin3g  5991  op2ndb  6258  ordintdif  6445  knatar  7393  uniordint  7837  oawordeulem  8610  oeeulem  8657  naddov3  8736  iinfi  9486  dfttrcl2  9793  tcsni  9812  rankval2  9887  rankval3b  9895  cf0  10320  cfval2  10329  cofsmo  10338  isf34lem4  10446  isf34lem7  10448  sstskm  10911  dfnn3  12307  trclun  15063  cycsubg  19248  efgval2  19766  00lsp  21002  alexsublem  24073  noextendlt  27732  nosepne  27743  nosepdm  27747  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem4  27799  bday0s  27891  intimafv  32722  dynkin  34131  imaiinfv  42649  elrfi  42650  onuniintrab  43187  naddov4  43345  naddwordnexlem4  43363  harval3  43500  relintab  43545  dfid7  43574  clcnvlem  43585  dfrtrcl5  43591  dfrcl2  43636  aiotajust  46999  dfaiota2  47001  ipolub0  48664