Theorem inteqd 4881

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-ral 3068  df-int 4877

This theorem is referenced by:  intprgOLD  4912  elreldm  5833  ordintdif  6300  fniinfv  6828  onsucmin  7643  elxp5  7744  1stval2  7821  2ndval2  7822  fundmen  8775  xpsnen  8796  unblem2  8997  unblem3  8998  fiint  9021  elfi2  9103  fi0  9109  elfiun  9119  tcvalg  9427  tz9.12lem3  9478  rankvalb  9486  rankvalg  9506  ranksnb  9516  rankonidlem  9517  cardval3  9641  cardidm  9648  harsucnn  9687  cfval  9934  cflim3  9949  coftr  9960  isfin3ds  10016  fin23lem17  10025  fin23lem39  10037  isf33lem  10053  isf34lem5  10065  isf34lem6  10067  wuncval  10429  tskmval  10526  cleq1  14622  dfrtrcl2  14701  mrcfval  17234  mrcval  17236  cycsubg2  18744  efgval  19238  lspfval  20150  lspval  20152  lsppropd  20195  aspval  20987  aspval2  21012  clsfval  22084  clsval  22096  clsval2  22109  hauscmplem  22465  cmpfi  22467  1stcfb  22504  fclscmp  23089  spanval  29596  chsupid  29675  intimafv  30945  zarclsint  31724  zarcmplem  31733  sigagenval  32008  kur14  33078  mclsval  33425  naddcllem  33758  naddov2  33761  naddcom  33762  naddid1  33763  scutval  33921  igenval  36146  pclfvalN  37830  pclvalN  37831  diaintclN  38999  docaffvalN  39062  docafvalN  39063  docavalN  39064  dibintclN  39108  dihglb2  39283  dihintcl  39285  mzpval  40470  dnnumch3lem  40787  aomclem8  40802  rgspnval  40909  iotain  41924  salgenval  43752  mreclat  46171