Theorem inteqd 4895

Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
inteqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
inteqd	⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Proof of Theorem inteqd

Step	Hyp	Ref	Expression
1		inteqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		inteq 4893	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1542  ∩ cint 4890

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 3063  df-int 4891

This theorem is referenced by:  elreldm  5884  ordintdif  6368  fniinfv  6912  onsucmin  7765  elxp5  7867  1stval2  7952  2ndval2  7953  naddcllem  8605  naddov2  8608  naddcom  8611  naddrid  8612  naddasslem1  8623  naddasslem2  8624  naddass  8625  naddsuc2  8630  fundmen  8971  xpsnen  8992  unblem2  9196  unblem3  9197  fiint  9230  elfi2  9320  fi0  9326  elfiun  9336  tcvalg  9648  tz9.12lem3  9704  rankvalb  9712  rankvalg  9732  ranksnb  9742  rankonidlem  9743  cardval3  9867  cardidm  9874  harsucnn  9913  cfval  10160  cflim3  10175  coftr  10186  isfin3ds  10242  fin23lem17  10251  fin23lem39  10263  isf33lem  10279  isf34lem5  10291  isf34lem6  10293  wuncval  10656  tskmval  10753  cleq1  14936  dfrtrcl2  15015  mrcfval  17565  mrcval  17567  cycsubg2  19176  efgval  19683  rgspnval  20580  lspfval  20959  lspval  20961  lsppropd  21005  aspval  21862  aspval2  21888  clsfval  23000  clsval  23012  clsval2  23025  hauscmplem  23381  cmpfi  23383  1stcfb  23420  fclscmp  24005  cutsval  27786  spanval  31419  chsupid  31498  intimafv  32799  fldgenval  33388  primefldgen1  33397  zarclsint  34032  zarcmplem  34041  sigagenval  34300  onvf1odlem3  35303  kur14  35414  mclsval  35761  igenval  38396  pclfvalN  40349  pclvalN  40350  diaintclN  41518  docaffvalN  41581  docafvalN  41582  docavalN  41583  dibintclN  41627  dihglb2  41802  dihintcl  41804  mzpval  43178  dnnumch3lem  43492  aomclem8  43507  rp-intrabeq  43667  nadd1suc  43838  minregex2  43980  iotain  44862  salgenval  46767  mreclat  49484