Description: Negation of subclass expressed in terms of intersection and proper subclass. (Contributed by NM, 30-Jun-2004) (Proof shortened by Andrew Salmon, 26-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nssinpss | |- ( -. A C_ B <-> ( A i^i B ) C. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | inss1 | |- ( A i^i B ) C_ A |
|
| 2 | 1 | biantrur | |- ( ( A i^i B ) =/= A <-> ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) ) |
| 3 | df-ss | |- ( A C_ B <-> ( A i^i B ) = A ) |
|
| 4 | 3 | necon3bbii | |- ( -. A C_ B <-> ( A i^i B ) =/= A ) |
| 5 | df-pss | |- ( ( A i^i B ) C. A <-> ( ( A i^i B ) C_ A /\ ( A i^i B ) =/= A ) ) |
|
| 6 | 2 4 5 | 3bitr4i | |- ( -. A C_ B <-> ( A i^i B ) C. A ) |