Theorem inteqd 4922

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ∩ cint 4917

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-ral 3083  df-rex 3093  df-int 4918

This theorem is used by:  elreldm  5930  ordintdif  6419  fniinfv  6966  onsucmin  7826  elxp5  7929  1stval2  8012  2ndval2  8013  naddcllem  8671  naddov2  8674  naddcom  8678  naddrid  8679  naddasslem1  8690  naddasslem2  8691  naddass  8692  naddsuc2  8697  fundmen  9038  xpsnen  9059  unblem2  9263  unblem3  9264  fiint  9296  elfi2  9384  fi0  9390  elfiun  9400  tcvalg  9715  tz9.12lem3  9771  rankvalb  9779  rankvalg  9799  ranksnb  9809  rankonidlem  9810  cardval3  9957  cardidm  9964  harsucnn  10003  cfval  10248  cflim3  10264  coftr  10275  isfin3ds  10331  fin23lem17  10340  fin23lem39  10352  isf33lem  10368  isf34lem5  10380  isf34lem6  10382  wuncval  10745  tskmval  10842  cleq1  15046  dfrtrcl2  15125  mrcfval  17689  mrcval  17691  cycsubg2  19312  efgval  19818  rgspnval  20748  lspfval  21131  lspval  21133  lsppropd  21176  rspvalint  21406  aspval  22059  aspval2  22085  clsfval  23219  clsval  23231  clsval2  23244  hauscmplem  23600  cmpfi  23602  1stcfb  23639  fclscmp  24224  cutsval  28010  spanval  31722  chsupid  31801  intimafv  33093  fldgenval  33664  primefldgen1  33673  zarclsint  34293  zarcmplem  34302  sigagenval  34562  onvf1odlem3  35613  onvfowev  35624  kur14  35729  mclsval  36076  nmulprop  36703  nmulcom  36707  nmulrid  36710  igenval  38753  pclfvalN  40704  pclvalN  40705  diaintclN  41873  docaffvalN  41936  docafvalN  41937  docavalN  41938  dibintclN  41982  dihglb2  42157  dihintcl  42159  mzpval  43504  dnnumch3lem  43814  aomclem8  43829  rp-intrabeq  43989  nadd1suc  44160  minregex2  44302  iotain  45168  salgenval  47076  mreclat  49816