Theorem inteqd 4754

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

Syntax hints:   → wi 4   = wceq 1507  ∩ cint 4749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-ral 3094  df-int 4750

This theorem is referenced by:  intprg  4783  elreldm  5648  ordintdif  6078  fniinfv  6570  onsucmin  7352  elxp5  7443  1stval2  7518  2ndval2  7519  fundmen  8380  xpsnen  8397  unblem2  8566  unblem3  8567  fiint  8590  elfi2  8673  fi0  8679  elfiun  8689  tcvalg  8974  tz9.12lem3  9012  rankvalb  9020  rankvalg  9040  ranksnb  9050  rankonidlem  9051  cardval3  9175  cardidm  9182  cfval  9467  cflim3  9482  coftr  9493  isfin3ds  9549  fin23lem17  9558  fin23lem39  9570  isf33lem  9586  isf34lem5  9598  isf34lem6  9600  wuncval  9962  tskmval  10059  cleq1  14204  dfrtrcl2  14282  mrcfval  16737  mrcval  16739  cycsubg2  18100  efgval  18601  lspfval  19467  lspval  19469  lsppropd  19512  aspval  19822  aspval2  19841  clsfval  21337  clsval  21349  clsval2  21362  hauscmplem  21718  cmpfi  21720  1stcfb  21757  fclscmp  22342  spanval  28891  chsupid  28970  sigagenval  31041  kur14  32045  mclsval  32327  scutval  32783  igenval  34778  pclfvalN  36467  pclvalN  36468  diaintclN  37636  docaffvalN  37699  docafvalN  37700  docavalN  37701  dibintclN  37745  dihglb2  37920  dihintcl  37922  mzpval  38721  dnnumch3lem  39039  aomclem8  39054  rgspnval  39161  iotain  40163  salgenval  42035