theorem ssv1 (A: set): $ _V C_ A <-> A == _V $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssasym | A C_ _V -> _V C_ A -> A == _V |
|
2 | ssv2 | A C_ _V |
|
3 | 1, 2 | ax_mp | _V C_ A -> A == _V |
4 | ssid | _V C_ _V |
|
5 | sseq2 | A == _V -> (_V C_ A <-> _V C_ _V) |
|
6 | 4, 5 | mpbiri | A == _V -> _V C_ A |
7 | 3, 6 | ibii | _V C_ A <-> A == _V |