Theorem inteqd 4915

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

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

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 4911

This theorem is referenced by:  elreldm  5899  ordintdif  6383  fniinfv  6939  onsucmin  7796  elxp5  7899  1stval2  7985  2ndval2  7986  naddcllem  8640  naddov2  8643  naddcom  8646  naddrid  8647  naddasslem1  8658  naddasslem2  8659  naddass  8660  naddsuc2  8665  fundmen  9002  xpsnen  9025  unblem2  9240  unblem3  9241  fiint  9277  fiintOLD  9278  elfi2  9365  fi0  9371  elfiun  9381  tcvalg  9691  tz9.12lem3  9742  rankvalb  9750  rankvalg  9770  ranksnb  9780  rankonidlem  9781  cardval3  9905  cardidm  9912  harsucnn  9951  cfval  10200  cflim3  10215  coftr  10226  isfin3ds  10282  fin23lem17  10291  fin23lem39  10303  isf33lem  10319  isf34lem5  10331  isf34lem6  10333  wuncval  10695  tskmval  10792  cleq1  14949  dfrtrcl2  15028  mrcfval  17569  mrcval  17571  cycsubg2  19142  efgval  19647  rgspnval  20521  lspfval  20879  lspval  20881  lsppropd  20925  aspval  21782  aspval2  21807  clsfval  22912  clsval  22924  clsval2  22937  hauscmplem  23293  cmpfi  23295  1stcfb  23332  fclscmp  23917  scutval  27712  spanval  31262  chsupid  31341  intimafv  32634  fldgenval  33262  primefldgen1  33271  zarclsint  33862  zarcmplem  33871  sigagenval  34130  onvf1odlem3  35092  kur14  35203  mclsval  35550  igenval  38055  pclfvalN  39883  pclvalN  39884  diaintclN  41052  docaffvalN  41115  docafvalN  41116  docavalN  41117  dibintclN  41161  dihglb2  41336  dihintcl  41338  mzpval  42720  dnnumch3lem  43035  aomclem8  43050  rp-intrabeq  43210  nadd1suc  43381  minregex2  43524  iotain  44406  salgenval  46319  mreclat  48985