Theorem difeq2d 2726

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

Syntax hints:   -> wi 3   = wceq 1298   \ cdif 2590

This theorem is referenced by:  imain 4494  dffv2 4734  tz7.49 5168  oev2 5207  sbthlem2 5511  sbthlem3 5512  sbth 5520  phplem3 5604  unblem2 5634  unblem3 5635  kmlem9 5935  kmlem11 5937  kmlem12 5938  alephsuc3 8854  clsval2 8961  ntrval2 8962  cmclsopn 8969  cmntrcld 8970  islp 9020  bcthlem15 9291  bcthlem16 9292  drngi 9493  dif1enOLD 10173  fixp 10180  rcfpfillem6 14933  ntrcmp 15406  clscmp 15407  clsun 15413  fimax 15746  inficl 15757  frfi 15771  heiborlem3 15957  heiborlem8 15962  isdivrngNEW 17160  invrfval 17170  watomfval 17392  watomval 17393

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rab 2112  df-dif 2597

Copyright terms: Public domain