Theorem ssdif0 2331

Description: Subclass expressed in terms of difference. Exercise 7 of [TakeutiZaring] p. 22.

Assertion

Ref	Expression
ssdif0	|- (A (_ B <-> (A \ B) = (/))

Proof of Theorem ssdif0

Step	Hyp	Ref	Expression
1		iman 237	. . . 4 |- ((x e. A -> x e. B) <-> -. (x e. A /\ -. x e. B))
2		eldif 2060	. . . . 5 |- (x e. (A \ B) <-> (x e. A /\ -. x e. B))
3	2	negbii 187	. . . 4 |- (-. x e. (A \ B) <-> -. (x e. A /\ -. x e. B))
4	1, 3	bitr4 176	. . 3 |- ((x e. A -> x e. B) <-> -. x e. (A \ B))
5	4	albii 1001	. 2 |- (A.x(x e. A -> x e. B) <-> A.x -. x e. (A \ B))
6		dfss2 2061	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
7		eq0 2298	. 2 |- ((A \ B) = (/) <-> A.x -. x e. (A \ B))
8	5, 6, 7	3bitr4 183	1 |- (A (_ B <-> (A \ B) = (/))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 956   = wceq 958   e. wcel 960   \ cdif 2047   (_ wss 2050  (/)c0 2283

This theorem is referenced by:  vdif0 2332  pssdifn0 2333  difid 2338  tfi 3132  peano5 3159  tz7.49 3965  oe0m1 4166  php3 4521  php3OLD 4522  0ntr 7699  bcthlem10 8005  strlem1 10172  rcfpfillem2 10564

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-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-in 2054  df-ss 2056  df-nul 2284

Copyright terms: Public domain