theorem ssasym (A B: set): $ A C_ B -> B C_ A -> A == B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ian | (x e. A -> x e. B) -> (x e. B -> x e. A) -> (x e. A -> x e. B) /\ (x e. B -> x e. A) |
|
| 2 | 1 | conv iff | (x e. A -> x e. B) -> (x e. B -> x e. A) -> (x e. A <-> x e. B) |
| 3 | 2 | al2imi | A. x (x e. A -> x e. B) -> A. x (x e. B -> x e. A) -> A. x (x e. A <-> x e. B) |
| 4 | 3 | conv eqs, subset | A C_ B -> B C_ A -> A == B |