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  6419  onsucmin  7186  elxp5  7276  1stval2  7350  2ndval2  7351  fundmen  8195  xpsnen  8209  unblem2  8378  unblem3  8379  fiint  8402  elfi2  8485  fi0  8491  elfiun  8501  tcvalg  8787  tz9.12lem3  8825  rankvalb  8833  rankvalg  8853  ranksnb  8863  rankonidlem  8864  cardval3  8968  cardidm  8975  cfval  9261  cflim3  9276  coftr  9287  isfin3ds  9343  fin23lem17  9352  fin23lem39  9364  isf33lem  9380  isf34lem5  9392  isf34lem6  9394  wuncval  9756  tskmval  9853  cleq1  13923  dfrtrcl2  14001  mrcfval  16470  mrcval  16472  cycsubg2  17832  efgval  18330  lspfval  19175  lspval  19177  lsppropd  19220  aspval  19530  aspval2  19549  clsfval  21031  clsval  21043  clsval2  21056  hauscmplem  21411  cmpfi  21413  1stcfb  21450  fclscmp  22035  spanval  28501  chsupid  28580  sigagenval  30512  kur14  31505  mclsval  31767  scutval  32217  igenval  34173  pclfvalN  35678  pclvalN  35679  diaintclN  36849  docaffvalN  36912  docafvalN  36913  docavalN  36914  dibintclN  36958  dihglb2  37133  dihintcl  37135  mzpval  37797  dnnumch3lem  38118  aomclem8  38133  rgspnval  38240  iotain  39120  salgenval  41044