Theorem ineq1d 2268

Description: Equality deduction for intersection of two classes.

Hypothesis

Ref	Expression
ineq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
ineq1d	⊢ (φ → (A ∩ C) = (B ∩ C))

Proof of Theorem ineq1d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (φ → A = B)
2		ineq1 2262	. 2 ⊢ (A = B → (A ∩ C) = (B ∩ C))
3	1, 2	syl 10	1 ⊢ (φ → (A ∩ C) = (B ∩ C))

Syntax hints:   → wi 3   = wceq 992   ∩ cin 2098

This theorem is referenced by:  ineq12d 2270  fnresdisj 3703  funimadisj 3712  fiint 4703  kmlem12 4922  limsupval 6724  subtop 7858  indistop 7860  bcthlem15 8224  chdmj2 9729  cmcmlem 9810  pjoml2 9830  fh2 9838  mdbr 10502  mdi 10503  mdbr3 10505  mdbr4 10506  dmdmd 10508  dmdbr3 10513  dmdbr4 10514  dmdi4 10515  dmdbr5 10516  mddmd2 10517  mdsl1i 10529  cvmdi 10532  mdslmd1lem1 10533  mdslmd1lem2 10534  mdslmd1lem3 10535  mdslmd1lem4 10536  mdslmd1i 10537  mdslmd3i 10540  csmdsymi 10542  mdexchi 10543  atomli 10591  atabsi 10610  sumdmdlem2 10628  dmdbr5ati 10631  bwt2 11123  compcov 11486  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem4 11499  alexsub 11500  metsstop 11909  totbndss 11993  heiborlem1 12011  heiborlem9 12019  heiborlem23 12033  heiborlem28 12038  heiborlem30 12040  heiborlem31 12041  heiborlem42 12052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103

Copyright terms: Public domain