theorem inss2 (A B: set): $ A i^i B C_ B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sseq1 | B i^i A == A i^i B -> (B i^i A C_ B <-> A i^i B C_ B) |
|
| 2 | incom | B i^i A == A i^i B |
|
| 3 | 1, 2 | ax_mp | B i^i A C_ B <-> A i^i B C_ B |
| 4 | inss1 | B i^i A C_ B |
|
| 5 | 3, 4 | mpbi | A i^i B C_ B |