Theorem disjdif 3519

Description: A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)

Assertion

Ref	Expression
disjdif	|- ( A i^i ( B \ A ) ) = (/)

Proof of Theorem disjdif

Step	Hyp	Ref	Expression
1		inss1 3379	. 2 |- ( A i^i B ) C_ A
2		inssdif0im 3514	. 2 |- ( ( A i^i B ) C_ A -> ( A i^i ( B \ A ) ) = (/) )
3	1, 2	ax-mp 5	1 |- ( A i^i ( B \ A ) ) = (/)

Syntax hints:   = wceq 1364   \ cdif 3150   i^i cin 3152   C_ wss 3153   (/)c0 3446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3447

This theorem is referenced by:  ssdifin0  3528  difdifdirss  3531  fvsnun1  5755  fvsnun2  5756  phplem2  6909  unfiin  6982  xpfi  6986  sbthlem7  7022  sbthlemi8  7023  exmidfodomrlemim  7261  fihashssdif  10889  zfz1isolem1  10911  fsumlessfi  11603  fprodsplit1f  11777  setsfun  12653  setsfun0  12654  setsslid  12669