HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ssdif0 2323
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
StepHypRef Expression
1 iman 237 . . . 4 |- ((x e. A -> x e. B) <-> -. (x e. A /\ -. x e. B))
2 eldif 2053 . . . . 5 |- (x e. (A \ B) <-> (x e. A /\ -. x e. B))
32negbii 187 . . . 4 |- (-. x e. (A \ B) <-> -. (x e. A /\ -. x e. B))
41, 3bitr4 176 . . 3 |- ((x e. A -> x e. B) <-> -. x e. (A \ B))
54albii 997 . 2 |- (A.x(x e. A -> x e. B) <-> A.x -. x e. (A \ B))
6 dfss2 2054 . 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
7 eq0 2290 . 2 |- ((A \ B) = (/) <-> A.x -. x e. (A \ B))
85, 6, 73bitr4 183 1 |- (A (_ B <-> (A \ B) = (/))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956   \ cdif 2040   (_ wss 2043  (/)c0 2276
This theorem is referenced by:  vdif0 2324  pssdifn0 2325  difid 2330  tfi 3121  peano5 3148  tz7.49 3950  oe0m1 4150  php3 4501  0ntr 7652  bcthlem10 7958  strlem1 10115
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-in 2047  df-ss 2049  df-nul 2277
Copyright terms: Public domain