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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-ral 3059  df-rex 3068  df-int 4951

This theorem is referenced by:  elreldm  5948  ordintdif  6435  fniinfv  6986  onsucmin  7840  elxp5  7945  1stval2  8029  2ndval2  8030  naddcllem  8712  naddov2  8715  naddcom  8718  naddrid  8719  naddasslem1  8730  naddasslem2  8731  naddass  8732  naddsuc2  8737  fundmen  9069  xpsnen  9093  unblem2  9326  unblem3  9327  fiint  9363  fiintOLD  9364  elfi2  9451  fi0  9457  elfiun  9467  tcvalg  9775  tz9.12lem3  9826  rankvalb  9834  rankvalg  9854  ranksnb  9864  rankonidlem  9865  cardval3  9989  cardidm  9996  harsucnn  10035  cfval  10284  cflim3  10299  coftr  10310  isfin3ds  10366  fin23lem17  10375  fin23lem39  10387  isf33lem  10403  isf34lem5  10415  isf34lem6  10417  wuncval  10779  tskmval  10876  cleq1  15018  dfrtrcl2  15097  mrcfval  17652  mrcval  17654  cycsubg2  19240  efgval  19749  rgspnval  20628  lspfval  20988  lspval  20990  lsppropd  21034  aspval  21910  aspval2  21935  clsfval  23048  clsval  23060  clsval2  23073  hauscmplem  23429  cmpfi  23431  1stcfb  23468  fclscmp  24053  scutval  27859  spanval  31361  chsupid  31440  intimafv  32725  fldgenval  33293  primefldgen1  33302  zarclsint  33832  zarcmplem  33841  sigagenval  34120  kur14  35200  mclsval  35547  igenval  38047  pclfvalN  39871  pclvalN  39872  diaintclN  41040  docaffvalN  41103  docafvalN  41104  docavalN  41105  dibintclN  41149  dihglb2  41324  dihintcl  41326  mzpval  42719  dnnumch3lem  43034  aomclem8  43049  rp-intrabeq  43209  nadd1suc  43381  minregex2  43524  iotain  44412  salgenval  46276  mreclat  48785