Theorem inteqi 4701

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

Syntax hints:   = wceq 1656  ∩ cint 4697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-int 4698

This theorem is referenced by:  elintrab  4709  ssintrab  4720  intmin2  4724  intsng  4732  intexrab  5045  intabs  5047  op1stb  5160  dfiin3g  5612  op2ndb  5861  ordintdif  6012  knatar  6862  uniordint  7267  oawordeulem  7901  oeeulem  7948  iinfi  8592  tcsni  8896  rankval2  8958  rankval3b  8966  cf0  9388  cfval2  9397  cofsmo  9406  isf34lem4  9514  isf34lem7  9516  sstskm  9979  dfnn3  11366  trclun  14132  cycsubg  17973  efgval2  18488  00lsp  19340  alexsublem  22218  dynkin  30764  noextendlt  32350  nosepne  32359  nosepdm  32362  nosupbnd2lem1  32389  noetalem3  32393  imaiinfv  38093  elrfi  38094  relintab  38723  dfid7  38753  clcnvlem  38764  dfrtrcl5  38770  dfrcl2  38800  aiotajust  41974  dfaiota2  41976