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 18	1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-rex 3090  df-int 4914

This theorem is referenced by:  elreldm  5927  ordintdif  6414  fniinfv  6961  onsucmin  7818  elxp5  7921  1stval2  8004  2ndval2  8005  naddcllem  8663  naddov2  8666  naddcom  8670  naddrid  8671  naddasslem1  8682  naddasslem2  8683  naddass  8684  naddsuc2  8689  fundmen  9029  xpsnen  9050  unblem2  9254  unblem3  9255  fiint  9287  elfi2  9375  fi0  9381  elfiun  9391  tcvalg  9706  tz9.12lem3  9762  rankvalb  9770  rankvalg  9790  ranksnb  9800  rankonidlem  9801  cardval3  9939  cardidm  9946  harsucnn  9985  cfval  10231  cflim3  10247  coftr  10258  isfin3ds  10314  fin23lem17  10323  fin23lem39  10335  isf33lem  10351  isf34lem5  10363  isf34lem6  10365  wuncval  10728  tskmval  10825  cleq1  15022  dfrtrcl2  15101  mrcfval  17665  mrcval  17667  cycsubg2  19282  efgval  19788  rgspnval  20698  lspfval  21075  lspval  21077  lsppropd  21120  rspvalint  21350  aspval  22003  aspval2  22029  clsfval  23163  clsval  23175  clsval2  23188  hauscmplem  23544  cmpfi  23546  1stcfb  23583  fclscmp  24168  cutsval  27951  spanval  31663  chsupid  31742  intimafv  33034  fldgenval  33611  primefldgen1  33620  zarclsint  34240  zarcmplem  34249  sigagenval  34508  onvf1odlem3  35567  onvfowev  35578  kur14  35686  mclsval  36033  nmulprop  36660  nmulcom  36664  nmulrid  36675  igenval  38690  pclfvalN  40641  pclvalN  40642  diaintclN  41810  docaffvalN  41873  docafvalN  41874  docavalN  41875  dibintclN  41919  dihglb2  42094  dihintcl  42096  mzpval  43443  dnnumch3lem  43753  aomclem8  43768  rp-intrabeq  43928  nadd1suc  44099  minregex2  44241  iotain  45107  salgenval  47015  mreclat  49752