Theorem inteqi 4903

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

Syntax hints:   = wceq 1540  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-rex 3054  df-int 4900

This theorem is referenced by:  elintrab  4913  ssintrab  4924  intmin2  4928  intsng  4936  intexrab  5289  intabs  5291  op1stb  5418  dfiin3g  5914  op2ndb  6180  ordintdif  6362  knatar  7298  uniordint  7741  oawordeulem  8479  oeeulem  8526  naddov3  8605  iinfi  9326  dfttrcl2  9639  tcsni  9658  rankval2  9733  rankval3b  9741  cf0  10164  cfval2  10173  cofsmo  10182  isf34lem4  10290  isf34lem7  10292  sstskm  10755  dfnn3  12160  trclun  14939  cycsubg  19105  efgval2  19621  00lsp  20902  alexsublem  23947  noextendlt  27597  nosepne  27608  nosepdm  27612  nosupbnd2lem1  27643  noinfbnd2lem1  27658  noetasuplem4  27664  bday0s  27760  intimafv  32667  dynkin  34133  tz9.1regs  35066  imaiinfv  42666  elrfi  42667  onuniintrab  43199  naddov4  43356  naddwordnexlem4  43374  harval3  43511  relintab  43556  dfid7  43585  clcnvlem  43596  dfrtrcl5  43602  dfrcl2  43647  aiotajust  47069  dfaiota2  47071  ipolub0  48977