Theorem inteqd 4632

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

Syntax hints:   → wi 4   = wceq 1632  ∩ cint 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-int 4628

This theorem is referenced by:  intprg  4663  elreldm  5505  ordintdif  5935  fniinfv  6420  onsucmin  7187  elxp5  7277  1stval2  7351  2ndval2  7352  fundmen  8197  xpsnen  8211  unblem2  8380  unblem3  8381  fiint  8404  elfi2  8487  fi0  8493  elfiun  8503  tcvalg  8789  tz9.12lem3  8827  rankvalb  8835  rankvalg  8855  ranksnb  8865  rankonidlem  8866  cardval3  8988  cardidm  8995  cfval  9281  cflim3  9296  coftr  9307  isfin3ds  9363  fin23lem17  9372  fin23lem39  9384  isf33lem  9400  isf34lem5  9412  isf34lem6  9414  wuncval  9776  tskmval  9873  cleq1  13943  dfrtrcl2  14021  mrcfval  16490  mrcval  16492  cycsubg2  17852  efgval  18350  lspfval  19195  lspval  19197  lsppropd  19240  aspval  19550  aspval2  19569  clsfval  21051  clsval  21063  clsval2  21076  hauscmplem  21431  cmpfi  21433  1stcfb  21470  fclscmp  22055  spanval  28522  chsupid  28601  sigagenval  30533  kur14  31526  mclsval  31788  scutval  32238  igenval  34191  pclfvalN  35696  pclvalN  35697  diaintclN  36867  docaffvalN  36930  docafvalN  36931  docavalN  36932  dibintclN  36976  dihglb2  37151  dihintcl  37153  mzpval  37815  dnnumch3lem  38136  aomclem8  38151  rgspnval  38258  iotain  39138  salgenval  41062