Theorem ssdif0 2327

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 2057	. . . . 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 999	. 2 |- (A.x(x e. A -> x e. B) <-> A.x -. x e. (A \ B))
6		dfss2 2058	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
7		eq0 2294	. 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 954   = wceq 956   e. wcel 958   \ cdif 2044   (_ wss 2047  (/)c0 2280

This theorem is referenced by:  vdif0 2328  pssdifn0 2329  difid 2334  tfi 3126  peano5 3153  tz7.49 3959  oe0m1 4160  php3 4515  php3OLD 4516  0ntr 7702  bcthlem10 8008  strlem1 10177  rcfpfillem2 10587  rcfpfillem2OLD 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-in 2051  df-ss 2053  df-nul 2281

Copyright terms: Public domain