Theorem inteqd 4927

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

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

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-ral 3052  df-rex 3061  df-int 4923

This theorem is referenced by:  elreldm  5915  ordintdif  6403  fniinfv  6957  onsucmin  7815  elxp5  7919  1stval2  8005  2ndval2  8006  naddcllem  8688  naddov2  8691  naddcom  8694  naddrid  8695  naddasslem1  8706  naddasslem2  8707  naddass  8708  naddsuc2  8713  fundmen  9045  xpsnen  9069  unblem2  9301  unblem3  9302  fiint  9338  fiintOLD  9339  elfi2  9426  fi0  9432  elfiun  9442  tcvalg  9752  tz9.12lem3  9803  rankvalb  9811  rankvalg  9831  ranksnb  9841  rankonidlem  9842  cardval3  9966  cardidm  9973  harsucnn  10012  cfval  10261  cflim3  10276  coftr  10287  isfin3ds  10343  fin23lem17  10352  fin23lem39  10364  isf33lem  10380  isf34lem5  10392  isf34lem6  10394  wuncval  10756  tskmval  10853  cleq1  15002  dfrtrcl2  15081  mrcfval  17620  mrcval  17622  cycsubg2  19193  efgval  19698  rgspnval  20572  lspfval  20930  lspval  20932  lsppropd  20976  aspval  21833  aspval2  21858  clsfval  22963  clsval  22975  clsval2  22988  hauscmplem  23344  cmpfi  23346  1stcfb  23383  fclscmp  23968  scutval  27764  spanval  31314  chsupid  31393  intimafv  32688  fldgenval  33306  primefldgen1  33315  zarclsint  33903  zarcmplem  33912  sigagenval  34171  kur14  35238  mclsval  35585  igenval  38085  pclfvalN  39908  pclvalN  39909  diaintclN  41077  docaffvalN  41140  docafvalN  41141  docavalN  41142  dibintclN  41186  dihglb2  41361  dihintcl  41363  mzpval  42755  dnnumch3lem  43070  aomclem8  43085  rp-intrabeq  43245  nadd1suc  43416  minregex2  43559  iotain  44441  salgenval  46350  mreclat  48971