Theorem inteqi 4889

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

Syntax hints:   = wceq 1542  ∩ cint 4885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-ral 3071  df-int 4886

This theorem is referenced by:  elintrab  4897  ssintrab  4908  intmin2  4912  intsng  4922  intexrab  5268  intabs  5270  op1stb  5390  dfiin3g  5873  op2ndb  6129  ordintdif  6314  knatar  7225  uniordint  7646  oawordeulem  8377  oeeulem  8424  iinfi  9164  dfttrcl2  9470  tcsni  9511  rankval2  9587  rankval3b  9595  cf0  10018  cfval2  10027  cofsmo  10036  isf34lem4  10144  isf34lem7  10146  sstskm  10609  dfnn3  11998  trclun  14736  cycsubg  18838  efgval2  19341  00lsp  20254  alexsublem  23206  intimafv  31052  dynkin  32144  noextendlt  33881  nosepne  33892  nosepdm  33896  nosupbnd2lem1  33927  noinfbnd2lem1  33942  noetasuplem4  33948  bday0s  34031  imaiinfv  40524  elrfi  40525  harval3  41134  relintab  41173  dfid7  41202  clcnvlem  41213  dfrtrcl5  41219  dfrcl2  41264  aiotajust  44555  dfaiota2  44557  ipolub0  46257