Theorem inteqi 4479

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

Syntax hints:   = wceq 1483  ∩ cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-int 4476

This theorem is referenced by:  elintrab  4488  ssintrab  4500  intmin2  4504  intsng  4512  intexrab  4823  intabs  4825  op1stb  4940  dfiin3g  5379  op2ndb  5619  ordintdif  5774  knatar  6607  bm2.5ii  7006  oawordeulem  7634  oeeulem  7681  iinfi  8323  tcsni  8619  rankval2  8681  rankval3b  8689  cf0  9073  cfval2  9082  cofsmo  9091  isf34lem4  9199  isf34lem7  9201  sstskm  9664  dfnn3  11034  trclun  13755  cycsubg  17622  efgval2  18137  00lsp  18981  alexsublem  21848  dynkin  30230  noextendlt  31822  nosepne  31831  nosepdm  31834  nosupbnd2lem1  31861  noetalem3  31865  imaiinfv  37256  elrfi  37257  relintab  37889  dfid7  37919  clcnvlem  37930  dfrtrcl5  37936  dfrcl2  37966