Theorem difeq2d 2149

Description: Deduction adding difference to the left in a class equality.

Hypothesis

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

Assertion

Ref	Expression
difeq2d	|- (ph -> (C \ A) = (C \ B))

Proof of Theorem difeq2d

Step	Hyp	Ref	Expression
1		difeq1d.1	. 2 |- (ph -> A = B)
2		difeq2 2144	. 2 |- (A = B -> (C \ A) = (C \ B))
3	1, 2	syl 10	1 |- (ph -> (C \ A) = (C \ B))

Syntax hints:   -> wi 3   = wceq 953   \ cdif 2034

This theorem is referenced by:  tz7.49 3944  oev2 4146  sbthlem2 4428  sbthlem3 4429  sbth 4437  phplem3 4490  unblem2 4518  unblem3 4519  kmlem9 4745  kmlem11 4747  kmlem12 4748  alephsuc3 7527  clsval2 7627  ntrval2 7628  cmclsopn 7635  cmntrcld 7636  islp 7685  bcthlem15 7947  bcthlem16 7948

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-dif 2039

Copyright terms: Public domain