Theorem inteqd 4955

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

Syntax hints:   → wi 4   = wceq 1542  ∩ cint 4950

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ral 3063  df-rex 3072  df-int 4951

This theorem is referenced by:  intprgOLD  4988  elreldm  5933  ordintdif  6412  fniinfv  6967  onsucmin  7806  elxp5  7911  1stval2  7989  2ndval2  7990  naddcllem  8672  naddov2  8675  naddcom  8678  naddrid  8679  naddasslem1  8690  naddasslem2  8691  naddass  8692  fundmen  9028  xpsnen  9052  unblem2  9293  unblem3  9294  fiint  9321  elfi2  9406  fi0  9412  elfiun  9422  tcvalg  9730  tz9.12lem3  9781  rankvalb  9789  rankvalg  9809  ranksnb  9819  rankonidlem  9820  cardval3  9944  cardidm  9951  harsucnn  9990  cfval  10239  cflim3  10254  coftr  10265  isfin3ds  10321  fin23lem17  10330  fin23lem39  10342  isf33lem  10358  isf34lem5  10370  isf34lem6  10372  wuncval  10734  tskmval  10831  cleq1  14927  dfrtrcl2  15006  mrcfval  17549  mrcval  17551  cycsubg2  19082  efgval  19580  lspfval  20577  lspval  20579  lsppropd  20622  aspval  21419  aspval2  21444  clsfval  22521  clsval  22533  clsval2  22546  hauscmplem  22902  cmpfi  22904  1stcfb  22941  fclscmp  23526  scutval  27291  spanval  30574  chsupid  30653  intimafv  31920  fldgenval  32391  primefldgen1  32400  zarclsint  32841  zarcmplem  32850  sigagenval  33127  kur14  34196  mclsval  34543  igenval  36918  pclfvalN  38749  pclvalN  38750  diaintclN  39918  docaffvalN  39981  docafvalN  39982  docavalN  39983  dibintclN  40027  dihglb2  40202  dihintcl  40204  mzpval  41456  dnnumch3lem  41774  aomclem8  41789  rgspnval  41896  rp-intrabeq  41956  nadd1suc  42128  naddsuc2  42129  minregex2  42272  iotain  43162  salgenval  45024  mreclat  47576