Theorem inteqd 4917

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 4915	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1540  ∩ cint 4912

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-ral 3046  df-rex 3055  df-int 4913

This theorem is referenced by:  elreldm  5901  ordintdif  6385  fniinfv  6941  onsucmin  7798  elxp5  7901  1stval2  7987  2ndval2  7988  naddcllem  8642  naddov2  8645  naddcom  8648  naddrid  8649  naddasslem1  8660  naddasslem2  8661  naddass  8662  naddsuc2  8667  fundmen  9004  xpsnen  9028  unblem2  9246  unblem3  9247  fiint  9283  fiintOLD  9284  elfi2  9371  fi0  9377  elfiun  9387  tcvalg  9697  tz9.12lem3  9748  rankvalb  9756  rankvalg  9776  ranksnb  9786  rankonidlem  9787  cardval3  9911  cardidm  9918  harsucnn  9957  cfval  10206  cflim3  10221  coftr  10232  isfin3ds  10288  fin23lem17  10297  fin23lem39  10309  isf33lem  10325  isf34lem5  10337  isf34lem6  10339  wuncval  10701  tskmval  10798  cleq1  14955  dfrtrcl2  15034  mrcfval  17575  mrcval  17577  cycsubg2  19148  efgval  19653  rgspnval  20527  lspfval  20885  lspval  20887  lsppropd  20931  aspval  21788  aspval2  21813  clsfval  22918  clsval  22930  clsval2  22943  hauscmplem  23299  cmpfi  23301  1stcfb  23338  fclscmp  23923  scutval  27718  spanval  31268  chsupid  31347  intimafv  32640  fldgenval  33268  primefldgen1  33277  zarclsint  33868  zarcmplem  33877  sigagenval  34136  kur14  35203  mclsval  35550  igenval  38050  pclfvalN  39878  pclvalN  39879  diaintclN  41047  docaffvalN  41110  docafvalN  41111  docavalN  41112  dibintclN  41156  dihglb2  41331  dihintcl  41333  mzpval  42713  dnnumch3lem  43028  aomclem8  43043  rp-intrabeq  43203  nadd1suc  43374  minregex2  43517  iotain  44399  salgenval  46312  mreclat  48973