Description: Negation of subclass relationship. Exercise 13 of TakeutiZaring p. 18. (Contributed by NM, 25-Feb-1996) (Proof shortened by Andrew Salmon, 21-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nss | |- ( -. A C_ B <-> E. x ( x e. A /\ -. x e. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exanali | |- ( E. x ( x e. A /\ -. x e. B ) <-> -. A. x ( x e. A -> x e. B ) ) |
|
| 2 | dfss2 | |- ( A C_ B <-> A. x ( x e. A -> x e. B ) ) |
|
| 3 | 1 2 | xchbinxr | |- ( E. x ( x e. A /\ -. x e. B ) <-> -. A C_ B ) |
| 4 | 3 | bicomi | |- ( -. A C_ B <-> E. x ( x e. A /\ -. x e. B ) ) |