Theorem difexg 3458

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 2735	. 2 |- (A \ B) C_ A
2		ssexg 3457	. 2 |- (((A \ B) C_ A /\ A e. C) -> (A \ B) e. _V)
3	1, 2	mpan 759	1 |- (A e. C -> (A \ B) e. _V)

Syntax hints:   -> wi 3   e. wcel 1300  _Vcvv 2292   \ cdif 2590   C_ wss 2593

This theorem is referenced by:  difex2 3802  difex2OLD 3803  elpwun 3855  oev 5198  fodomr 5547  limensuci 5600  unfilem3 5643  pwfilem 5660  infeq5 5727  kmlem11 5937  kmlem12 5938  acdc2lem2 8758  acdc5lem2 8761  infxpidmlem12 8832  infdif 8837  infdif2 8838  infpss 8843  cctop 8922  ablmul 9439  grothprim 10141  dif1enOLD 10173  indexfi 10174  dif1card 10177  findcard 10178  findcardOLD 10179  bnj113 12458  rcfpfillem3 14930  rcfpfillem6 14933  clindistop 14962  lteqtpos 15024  opncldf1 15402  cptclsscpt 15432  compfipin0lem 15435  compfipin0 15436  ufileu 15573  filufint 15574  ufinffr 15578  ufilen 15579  fcluscf 15612  flimfnfcls 15615  findcard2 15745  indexfiOLD 15755  zornn0 15764  frfi 15771  fdc 15812  heiborlem3 15957  heiborlem5 15959  heiborlem7 15961  heiborlem8 15962  isdivrng2 16111  pltval 16781  divrngmclNEW 17164  divrngidlemNEW 17165  divrngidNEW 17166  invrcl 17171  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-9 1307  ax-10 1308  ax-11 1309  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  ax-sep 3438

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605

Copyright terms: Public domain