theorem ssun1 (A B: set): $ A C_ A u. B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elun | x e. A u. B <-> x e. A \/ x e. B |
|
| 2 | orl | x e. A -> x e. A \/ x e. B |
|
| 3 | 1, 2 | sylibr | x e. A -> x e. A u. B |
| 4 | 3 | ax_gen | A. x (x e. A -> x e. A u. B) |
| 5 | 4 | conv subset | A C_ A u. B |