Theorem ineq2d 2269

Description: Equality deduction for intersection of two classes.

Hypothesis

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

Assertion

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

Proof of Theorem ineq2d

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

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

This theorem is referenced by:  ineq12d 2270  frirr 2954  fr2nr 2955  fr3nr 3138  reseq2 3456  resdisj 3556  isofrlem 4015  oev2 4298  kmlem11 4921  basis1 7826  eltg 7830  indistop 7860  clslp 7958  metssba 8019  bcthlem15 8224  omlsi 9522  pjoml 9545  chdmj3 9730  chdmj4 9731  ledi 9739  cmbr 9803  cmbr3 9827  pjoml3 9831  fh1 9837  fh2 9838  dmdbr 10507  dmdmd 10508  dmdbr5 10516  dmdsl3 10523  irredlem2 10600  irredlem3 10601  dmdbr6ati 10632  moec 10745  basmetres 11416  topbnd 11460  opnbnd 11461  cldbnd 11462  subsubtop 11479  cnsubsp2 11484  compsub 11488  reconnlem1 11507  elfg 11633  neifg 11644  fcluscomplem 11732  isfclusf 11737  fclsfneii 11740  subspabs 11903  heiborlem25 12035  heiborlem26 12036

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