Theorem ssdif0 2380

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 235	. . . 4 |- ((x e. A -> x e. B) <-> -. (x e. A /\ -. x e. B))
2		eldif 2109	. . . . 5 |- (x e. (A \ B) <-> (x e. A /\ -. x e. B))
3	2	notbii 185	. . . 4 |- (-. x e. (A \ B) <-> -. (x e. A /\ -. x e. B))
4	1, 3	bitr4i 174	. . 3 |- ((x e. A -> x e. B) <-> -. x e. (A \ B))
5	4	albii 1035	. 2 |- (A.x(x e. A -> x e. B) <-> A.x -. x e. (A \ B))
6		dfss2 2110	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
7		eq0 2347	. 2 |- ((A \ B) = (/) <-> A.x -. x e. (A \ B))
8	5, 6, 7	3bitr4i 181	1 |- (A (_ B <-> (A \ B) = (/))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994   \ cdif 2096   (_ wss 2099  (/)c0 2332

This theorem is referenced by:  vdif0 2381  pssdifn0 2382  difid 2387  tfi 3207  peano5 3241  tz7.49 4260  oe0m1 4296  php3 4662  0ntr 7912  bcthlem10 8219  strlem1 10458  rcfpfillem2 11090  clindistop 11131  dfcon2 11501  ufinffr 11663  inficl 11849

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-in 2103  df-ss 2105  df-nul 2333

Copyright terms: Public domain