theorem ssasymb (A B: set): $ A == B <-> A C_ B /\ B C_ A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqss | A == B -> A C_ B |
|
2 | eqssr | A == B -> B C_ A |
|
3 | 1, 2 | iand | A == B -> A C_ B /\ B C_ A |
4 | ssasym | A C_ B -> B C_ A -> A == B |
|
5 | 4 | imp | A C_ B /\ B C_ A -> A == B |
6 | 3, 5 | ibii | A == B <-> A C_ B /\ B C_ A |