Theorem inteqi 4907

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

Syntax hints:   = wceq 1542  ∩ cint 4903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rex 3062  df-int 4904

This theorem is referenced by:  elintrab  4916  ssintrab  4927  intmin2  4931  intsng  4939  intexrab  5293  intabs  5295  op1stb  5420  dfiin3g  5919  op2ndb  6186  ordintdif  6369  knatar  7305  uniordint  7748  oawordeulem  8483  oeeulem  8531  naddov3  8610  iinfi  9324  dfttrcl2  9637  tcsni  9654  rankval2  9734  rankval3b  9742  cf0  10165  cfval2  10174  cofsmo  10183  isf34lem4  10291  isf34lem7  10293  sstskm  10757  dfnn3  12163  trclun  14941  cycsubg  19141  efgval2  19657  00lsp  20936  alexsublem  23992  noextendlt  27641  nosepne  27652  nosepdm  27656  nosupbnd2lem1  27687  noinfbnd2lem1  27702  noetasuplem4  27708  bday0s  27809  intimafv  32771  dynkin  34305  rankval2b  35236  tz9.1regs  35271  imaiinfv  42971  elrfi  42972  onuniintrab  43504  naddov4  43661  naddwordnexlem4  43679  harval3  43815  relintab  43860  dfid7  43889  clcnvlem  43900  dfrtrcl5  43906  dfrcl2  43951  aiotajust  47366  dfaiota2  47368  ipolub0  49273