Theorem difeq2i 2159

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

Hypothesis

Ref	Expression
difeq1i.1	|- A = B

Assertion

Ref	Expression
difeq2i	|- (C \ A) = (C \ B)

Proof of Theorem difeq2i

Step	Hyp	Ref	Expression
1		difeq1i.1	. 2 |- A = B
2		difeq2 2157	. 2 |- (A = B -> (C \ A) = (C \ B))
3	1, 2	ax-mp 7	1 |- (C \ A) = (C \ B)

Syntax hints:   = wceq 958   \ cdif 2047

This theorem is referenced by:  difeq12i 2160  dfun3 2249  dfin3 2250  dfin4 2251  invdif 2252  indif 2253  difundi 2260  difindi 2262  dif23 2267  symdif1 2268  dif0 2339  undifv 2343  difdifdir 2350  dfsdom2 4466  numthlem 4793

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-dif 2052

Copyright terms: Public domain