Theorem difeq2d 2156

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 2151	. 2 |- (A = B -> (C \ A) = (C \ B))
3	1, 2	syl 10	1 |- (ph -> (C \ A) = (C \ B))

Syntax hints:   -> wi 3   = wceq 955   \ cdif 2041

This theorem is referenced by:  tz7.49 3954  oev2 4155  sbthlem2 4437  sbthlem3 4438  sbth 4446  phplem3 4499  unblem2 4527  unblem3 4528  kmlem9 4756  kmlem11 4758  kmlem12 4759  alephsuc3 7545  clsval2 7645  ntrval2 7646  cmclsopn 7653  cmntrcld 7654  islp 7704  bcthlem15 7975  bcthlem16 7976  rcfpfillem6 10516

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-dif 2046

Copyright terms: Public domain