Theorem difexg 2718

Description: Existence of a difference.

Assertion

Ref	Expression
difexg	|- (A e. C -> (A \ B) e. V)

Proof of Theorem difexg

Step	Hyp	Ref	Expression
1		difss 2164	. 2 |- (A \ B) (_ A
2		ssexg 2717	. 2 |- (((A \ B) (_ A /\ A e. C) -> (A \ B) e. V)
3	1, 2	mpan 694	1 |- (A e. C -> (A \ B) e. V)

Syntax hints:   -> wi 3   e. wcel 957  Vcvv 1808   \ cdif 2041   (_ wss 2044

This theorem is referenced by:  difex2 2873  elpwun 2907  oev 4146  fodomr 4472  limensuci 4495  unfilem3 4535  pwfilem 4553  infeq5 4604  kmlem11 4758  kmlem12 4759  acdc2lem2 7448  acdc5lem2 7451  infxpidmlem12 7523  infdif 7528  infdif2 7529  infpss 7534  cctop 7612  ablmul 8095  grothprim 8738  rcfpfillem3 10513  rcfpfillem6 10516  dtopcl 10531

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  ax-sep 2699

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-v 1809  df-dif 2046  df-in 2048  df-ss 2050

Copyright terms: Public domain