Theorem inteqi 4873

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

Syntax hints:   = wceq 1533  ∩ cint 4869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-int 4870

This theorem is referenced by:  elintrab  4881  ssintrab  4892  intmin2  4896  intsng  4904  intexrab  5236  intabs  5238  op1stb  5356  dfiin3g  5831  op2ndb  6079  ordintdif  6235  knatar  7104  uniordint  7515  oawordeulem  8174  oeeulem  8221  iinfi  8875  tcsni  9179  rankval2  9241  rankval3b  9249  cf0  9667  cfval2  9676  cofsmo  9685  isf34lem4  9793  isf34lem7  9795  sstskm  10258  dfnn3  11646  trclun  14368  cycsubg  18345  efgval2  18844  00lsp  19747  alexsublem  22646  dynkin  31421  noextendlt  33171  nosepne  33180  nosepdm  33183  nosupbnd2lem1  33210  noetalem3  33214  imaiinfv  39283  elrfi  39284  harval3  39897  relintab  39936  dfid7  39965  clcnvlem  39976  dfrtrcl5  39982  dfrcl2  40012  aiotajust  43277  dfaiota2  43279