Theorem ineq2d 2217

Description: Equality deduction for intersection of two classes.

Hypothesis

Ref	Expression
ineq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
ineq2d	|- (ph -> (C i^i A) = (C i^i B))

Proof of Theorem ineq2d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 |- (ph -> A = B)
2		ineq2 2211	. 2 |- (A = B -> (C i^i A) = (C i^i B))
3	1, 2	syl 10	1 |- (ph -> (C i^i A) = (C i^i B))

Syntax hints:   -> wi 3   = wceq 956   i^i cin 2046

This theorem is referenced by:  ineq12d 2218  frirr 2924  fr2nr 2925  fr3nr 2926  reseq2 3369  resdisj 3471  isofrlem 3901  oev2 4162  kmlem11 4775  basis1t 7614  eltgt 7618  indistop 7648  clslp 7748  metssba 7809  bcthlem15 8013  omls 9246  pjomlt 9269  chdmj3t 9454  chdmj4t 9455  ledit 9463  cmbrt 9527  cmbr3t 9551  pjoml3t 9555  fh1t 9561  fh2t 9562  dmdbrt 10226  dmdmdt 10227  dmdbr5 10235  dmdsl3t 10242  irredlem2 10318  irredlem3 10319  dmdbr6at 10350  moec 10461  sfvlimOLD 10606  limfillem2OLD 10608

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051

Copyright terms: Public domain