Description: Only the universal class has the universal class as a subclass. (Contributed by NM, 17-Sep-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | vss | |- ( _V C_ A <-> A = _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssv | |- A C_ _V |
|
| 2 | 1 | biantrur | |- ( _V C_ A <-> ( A C_ _V /\ _V C_ A ) ) |
| 3 | eqss | |- ( A = _V <-> ( A C_ _V /\ _V C_ A ) ) |
|
| 4 | 2 3 | bitr4i | |- ( _V C_ A <-> A = _V ) |