Theorem inteqd 4918

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

Syntax hints:   → wi 4   = wceq 1540  ∩ cint 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-ral 3046  df-rex 3055  df-int 4914

This theorem is referenced by:  elreldm  5902  ordintdif  6386  fniinfv  6942  onsucmin  7799  elxp5  7902  1stval2  7988  2ndval2  7989  naddcllem  8643  naddov2  8646  naddcom  8649  naddrid  8650  naddasslem1  8661  naddasslem2  8662  naddass  8663  naddsuc2  8668  fundmen  9005  xpsnen  9029  unblem2  9247  unblem3  9248  fiint  9284  fiintOLD  9285  elfi2  9372  fi0  9378  elfiun  9388  tcvalg  9698  tz9.12lem3  9749  rankvalb  9757  rankvalg  9777  ranksnb  9787  rankonidlem  9788  cardval3  9912  cardidm  9919  harsucnn  9958  cfval  10207  cflim3  10222  coftr  10233  isfin3ds  10289  fin23lem17  10298  fin23lem39  10310  isf33lem  10326  isf34lem5  10338  isf34lem6  10340  wuncval  10702  tskmval  10799  cleq1  14956  dfrtrcl2  15035  mrcfval  17576  mrcval  17578  cycsubg2  19149  efgval  19654  rgspnval  20528  lspfval  20886  lspval  20888  lsppropd  20932  aspval  21789  aspval2  21814  clsfval  22919  clsval  22931  clsval2  22944  hauscmplem  23300  cmpfi  23302  1stcfb  23339  fclscmp  23924  scutval  27719  spanval  31269  chsupid  31348  intimafv  32641  fldgenval  33269  primefldgen1  33278  zarclsint  33869  zarcmplem  33878  sigagenval  34137  onvf1odlem3  35099  kur14  35210  mclsval  35557  igenval  38062  pclfvalN  39890  pclvalN  39891  diaintclN  41059  docaffvalN  41122  docafvalN  41123  docavalN  41124  dibintclN  41168  dihglb2  41343  dihintcl  41345  mzpval  42727  dnnumch3lem  43042  aomclem8  43057  rp-intrabeq  43217  nadd1suc  43388  minregex2  43531  iotain  44413  salgenval  46326  mreclat  48989