Theorem inteqd 4480

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

Syntax hints:   → wi 4   = wceq 1483  ∩ cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-int 4476

This theorem is referenced by:  intprg  4511  elreldm  5350  ordintdif  5774  fniinfv  6257  onsucmin  7021  elxp5  7111  1stval2  7185  2ndval2  7186  fundmen  8030  xpsnen  8044  unblem2  8213  unblem3  8214  fiint  8237  elfi2  8320  fi0  8326  elfiun  8336  tcvalg  8614  tz9.12lem3  8652  rankvalb  8660  rankvalg  8680  ranksnb  8690  rankonidlem  8691  cardval3  8778  cardidm  8785  cfval  9069  cflim3  9084  coftr  9095  isfin3ds  9151  fin23lem17  9160  fin23lem39  9172  isf33lem  9188  isf34lem5  9200  isf34lem6  9202  wuncval  9564  tskmval  9661  cleq1  13722  dfrtrcl2  13802  mrcfval  16268  mrcval  16270  cycsubg2  17631  efgval  18130  lspfval  18973  lspval  18975  lsppropd  19018  aspval  19328  aspval2  19347  clsfval  20829  clsval  20841  clsval2  20854  hauscmplem  21209  cmpfi  21211  1stcfb  21248  fclscmp  21834  spanval  28192  chsupid  28271  sigagenval  30203  kur14  31198  mclsval  31460  scutval  31911  igenval  33860  pclfvalN  35175  pclvalN  35176  diaintclN  36347  docaffvalN  36410  docafvalN  36411  docavalN  36412  dibintclN  36456  dihglb2  36631  dihintcl  36633  mzpval  37295  dnnumch3lem  37616  aomclem8  37631  rgspnval  37738  iotain  38618  salgenval  40541