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 1541  ∩ cint 4950

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-ral 3062  df-rex 3071  df-int 4951

This theorem is referenced by:  intprgOLD  4988  elreldm  5934  ordintdif  6414  fniinfv  6969  onsucmin  7811  elxp5  7916  1stval2  7994  2ndval2  7995  naddcllem  8677  naddov2  8680  naddcom  8683  naddrid  8684  naddasslem1  8695  naddasslem2  8696  naddass  8697  fundmen  9033  xpsnen  9057  unblem2  9298  unblem3  9299  fiint  9326  elfi2  9411  fi0  9417  elfiun  9427  tcvalg  9735  tz9.12lem3  9786  rankvalb  9794  rankvalg  9814  ranksnb  9824  rankonidlem  9825  cardval3  9949  cardidm  9956  harsucnn  9995  cfval  10244  cflim3  10259  coftr  10270  isfin3ds  10326  fin23lem17  10335  fin23lem39  10347  isf33lem  10363  isf34lem5  10375  isf34lem6  10377  wuncval  10739  tskmval  10836  cleq1  14934  dfrtrcl2  15013  mrcfval  17556  mrcval  17558  cycsubg2  19125  efgval  19626  lspfval  20728  lspval  20730  lsppropd  20773  aspval  21646  aspval2  21671  clsfval  22749  clsval  22761  clsval2  22774  hauscmplem  23130  cmpfi  23132  1stcfb  23169  fclscmp  23754  scutval  27526  spanval  30841  chsupid  30920  intimafv  32187  fldgenval  32660  primefldgen1  32669  zarclsint  33138  zarcmplem  33147  sigagenval  33424  kur14  34493  mclsval  34840  igenval  37232  pclfvalN  39063  pclvalN  39064  diaintclN  40232  docaffvalN  40295  docafvalN  40296  docavalN  40297  dibintclN  40341  dihglb2  40516  dihintcl  40518  mzpval  41772  dnnumch3lem  42090  aomclem8  42105  rgspnval  42212  rp-intrabeq  42272  nadd1suc  42444  naddsuc2  42445  minregex2  42588  iotain  43478  salgenval  45336  mreclat  47710