Theorem inteqd 4884

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

Syntax hints:   → wi 4   = wceq 1539  ∩ cint 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-ral 3069  df-int 4880

This theorem is referenced by:  intprgOLD  4915  elreldm  5844  ordintdif  6315  fniinfv  6846  onsucmin  7668  elxp5  7770  1stval2  7848  2ndval2  7849  fundmen  8821  xpsnen  8842  unblem2  9067  unblem3  9068  fiint  9091  elfi2  9173  fi0  9179  elfiun  9189  tcvalg  9496  tz9.12lem3  9547  rankvalb  9555  rankvalg  9575  ranksnb  9585  rankonidlem  9586  cardval3  9710  cardidm  9717  harsucnn  9756  cfval  10003  cflim3  10018  coftr  10029  isfin3ds  10085  fin23lem17  10094  fin23lem39  10106  isf33lem  10122  isf34lem5  10134  isf34lem6  10136  wuncval  10498  tskmval  10595  cleq1  14694  dfrtrcl2  14773  mrcfval  17317  mrcval  17319  cycsubg2  18829  efgval  19323  lspfval  20235  lspval  20237  lsppropd  20280  aspval  21077  aspval2  21102  clsfval  22176  clsval  22188  clsval2  22201  hauscmplem  22557  cmpfi  22559  1stcfb  22596  fclscmp  23181  spanval  29695  chsupid  29774  intimafv  31043  zarclsint  31822  zarcmplem  31831  sigagenval  32108  kur14  33178  mclsval  33525  naddcllem  33831  naddov2  33834  naddcom  33835  naddid1  33836  scutval  33994  igenval  36219  pclfvalN  37903  pclvalN  37904  diaintclN  39072  docaffvalN  39135  docafvalN  39136  docavalN  39137  dibintclN  39181  dihglb2  39356  dihintcl  39358  mzpval  40554  dnnumch3lem  40871  aomclem8  40886  rgspnval  40993  minregex2  41142  iotain  42035  salgenval  43862  mreclat  46283